nat.lt
λn. λm. (n+1) ≤ m
Definition lt : nat -> nat -> Prop := fun (n:nat) => fun (m:nat) => le (S n) m
definition lt : nat -> nat -> Prop := \lambda n : nat. \lambda m : nat. (le) ((S) n) m
def lt : (nat.nat) -> (nat.nat) -> Prop := fun (n : nat.nat) , fun (m : nat.nat) , (((nat.le_) ) (((nat.S) ) (n))) (m)
lt : [nat_sttfa.sttfa_nat -> [nat_sttfa.sttfa_nat -> bool]] = (LAMBDA(n:nat_sttfa.sttfa_nat):(LAMBDA(m:nat_sttfa.sttfa_nat):nat_sttfa.le(nat_sttfa.sttfa_S(n))(m)))
Printing for OpenTheory is not working at the moment.