-Appl) w (lift1 is t)))))))))).(let H_x \def (leq_gen_head g a a0 a3 H3) in
-(let H7 \def H_x in (ex3_2_ind A A (\lambda (a4: A).(\lambda (a5: A).(eq A a3
-(AHead a4 a5)))) (\lambda (a4: A).(\lambda (_: A).(leq g a a4))) (\lambda (_:
-A).(\lambda (a5: A).(leq g a0 a5))) (sc3 g a3 c t) (\lambda (x0: A).(\lambda
-(x1: A).(\lambda (H8: (eq A a3 (AHead x0 x1))).(\lambda (H9: (leq g a
-x0)).(\lambda (H10: (leq g a0 x1)).(eq_ind_r A (AHead x0 x1) (\lambda (a4:
-A).(sc3 g a4 c t)) (conj (arity g c t (AHead x0 x1)) (\forall (d: C).(\forall
-(w: T).((sc3 g x0 d w) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g x1
-d (THead (Flat Appl) w (lift1 is t)))))))) (arity_repl g c t (AHead a a0) H5
-(AHead x0 x1) (leq_head g a x0 H9 a0 x1 H10)) (\lambda (d: C).(\lambda (w:
-T).(\lambda (H11: (sc3 g x0 d w)).(\lambda (is: PList).(\lambda (H12: (drop1
-is d c)).(H0 (\lambda (a4: A).(\lambda (H13: (llt a4 a0)).(\lambda (c0:
-C).(\lambda (t0: T).(\lambda (H14: (sc3 g a4 c0 t0)).(\lambda (a5:
-A).(\lambda (H15: (leq g a4 a5)).(H1 a4 (llt_trans a4 a0 (AHead a a0) H13
-(llt_head_dx a a0)) c0 t0 H14 a5 H15)))))))) d (THead (Flat Appl) w (lift1 is
-t)) (H6 d w (H1 x0 (llt_repl g a x0 H9 (AHead a a0) (llt_head_sx a a0)) d w
-H11 a (leq_sym g a x0 H9)) is H12) x1 H10))))))) a3 H8)))))) H7)))))
-H4)))))))))))) a2)) a1)).
+Appl) w (lift1 is t)))))))))).(let H_x \def (leq_gen_head1 g a a0 a3 H3) in
+(let H7 \def H_x in (ex3_2_ind A A (\lambda (a4: A).(\lambda (_: A).(leq g a
+a4))) (\lambda (_: A).(\lambda (a5: A).(leq g a0 a5))) (\lambda (a4:
+A).(\lambda (a5: A).(eq A a3 (AHead a4 a5)))) (sc3 g a3 c t) (\lambda (x0:
+A).(\lambda (x1: A).(\lambda (H8: (leq g a x0)).(\lambda (H9: (leq g a0
+x1)).(\lambda (H10: (eq A a3 (AHead x0 x1))).(let H11 \def (f_equal A A
+(\lambda (e: A).e) a3 (AHead x0 x1) H10) in (eq_ind_r A (AHead x0 x1)
+(\lambda (a4: A).(sc3 g a4 c t)) (conj (arity g c t (AHead x0 x1)) (\forall
+(d: C).(\forall (w: T).((sc3 g x0 d w) \to (\forall (is: PList).((drop1 is d
+c) \to (sc3 g x1 d (THead (Flat Appl) w (lift1 is t)))))))) (arity_repl g c t
+(AHead a a0) H5 (AHead x0 x1) (leq_head g a x0 H8 a0 x1 H9)) (\lambda (d:
+C).(\lambda (w: T).(\lambda (H12: (sc3 g x0 d w)).(\lambda (is:
+PList).(\lambda (H13: (drop1 is d c)).(H0 (\lambda (a4: A).(\lambda (H14:
+(llt a4 a0)).(\lambda (c0: C).(\lambda (t0: T).(\lambda (H15: (sc3 g a4 c0
+t0)).(\lambda (a5: A).(\lambda (H16: (leq g a4 a5)).(H1 a4 (llt_trans a4 a0
+(AHead a a0) H14 (llt_head_dx a a0)) c0 t0 H15 a5 H16)))))))) d (THead (Flat
+Appl) w (lift1 is t)) (H6 d w (H1 x0 (llt_repl g a x0 H8 (AHead a a0)
+(llt_head_sx a a0)) d w H12 a (leq_sym g a x0 H8)) is H13) x1 H9))))))) a3
+H11))))))) H7))))) H4)))))))))))) a2)) a1)).