-(subst0_gen_lift_ge u x3 x7 (s (Bind x0) i) (S O) O H24 (le_S_n (S O) (S i)
-(lt_le_S (S O) (S (S i)) (lt_n_S O (S i) (le_lt_n_Sm O i (le_O_n i))))))) x6
-H23)))) H22)) (\lambda (H22: (ex2 T (\lambda (t3: T).(eq T x6 (THead (Flat
-Appl) (lift (S O) O x3) t3))) (\lambda (t3: T).(subst0 (s (Flat Appl) (s
-(Bind x0) i)) u x5 t3)))).(ex2_ind T (\lambda (t3: T).(eq T x6 (THead (Flat
-Appl) (lift (S O) O x3) t3))) (\lambda (t3: T).(subst0 (s (Flat Appl) (s
-(Bind x0) i)) u x5 t3)) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
-T (THead (Bind x0) x4 x6) (THead (Flat Appl) u2 t3)))) (\lambda (u2:
+(subst0_gen_lift_ge u x3 x7 (s (Bind x0) i) (S O) O H24 (le_n_S O i (le_O_n
+i)))) x6 H23)))) H22)) (\lambda (H22: (ex2 T (\lambda (t3: T).(eq T x6 (THead
+(Flat Appl) (lift (S O) O x3) t3))) (\lambda (t3: T).(subst0 (s (Flat Appl)
+(s (Bind x0) i)) u x5 t3)))).(ex2_ind T (\lambda (t3: T).(eq T x6 (THead
+(Flat Appl) (lift (S O) O x3) t3))) (\lambda (t3: T).(subst0 (s (Flat Appl)
+(s (Bind x0) i)) u x5 t3)) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
+T).(eq T (THead (Bind x0) x4 x6) (THead (Flat Appl) u2 t3)))) (\lambda (u2: