-n0 n)) H5 (plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n
-(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O)))
-(plus_comm (S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal
-nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n
-(le_O_n d0) H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda
-(d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)
+n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n
+(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O))) (plus_sym
+(S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus
+O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0)
+H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d:
+C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst)