- \lambda (a1: A).(\lambda (a2: A).(le_S_n (S (lweight a1)) (S (plus (lweight
-a1) (lweight a2))) (le_n_S (S (lweight a1)) (S (plus (lweight a1) (lweight
-a2))) (le_n_S (lweight a1) (plus (lweight a1) (lweight a2)) (le_plus_l
-(lweight a1) (lweight a2)))))).
+ \lambda (a1: A).(\lambda (a2: A).(le_n_S (lweight a1) (plus (lweight a1)
+(lweight a2)) (le_plus_l (lweight a1) (lweight a2)))).