\forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
(n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
\forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
\def
\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda
(n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le
n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).