λ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.