-A).A) with [(ASort _ _) \Rightarrow a2 | (AHead _ a) \Rightarrow a])) (AHead
-a1 a2) (AHead a0 (asucc g a3)) H1) in (\lambda (H4: (eq A a1 a0)).(let H5
-\def (eq_ind_r A a0 (\lambda (a: A).((eq A (AHead a1 a2) (asucc g a)) \to
-(ex2 A (\lambda (a0: A).(eq A a (AHead a1 a0))) (\lambda (a0: A).(eq A a2
-(asucc g a0)))))) H a1 H4) in (eq_ind A a1 (\lambda (a4: A).(ex2 A (\lambda
-(a5: A).(eq A (AHead a4 a3) (AHead a1 a5))) (\lambda (a5: A).(eq A a2 (asucc
-g a5))))) (let H6 \def (eq_ind A a2 (\lambda (a: A).((eq A (AHead a1 a)
-(asucc g a3)) \to (ex2 A (\lambda (a0: A).(eq A a3 (AHead a1 a0))) (\lambda
-(a0: A).(eq A a (asucc g a0)))))) H0 (asucc g a3) H3) in (let H7 \def (eq_ind
-A a2 (\lambda (a: A).((eq A (AHead a1 a) (asucc g a1)) \to (ex2 A (\lambda
-(a0: A).(eq A a1 (AHead a1 a0))) (\lambda (a0: A).(eq A a (asucc g a0))))))
-H5 (asucc g a3) H3) in (eq_ind_r A (asucc g a3) (\lambda (a4: A).(ex2 A
-(\lambda (a5: A).(eq A (AHead a1 a3) (AHead a1 a5))) (\lambda (a5: A).(eq A
-a4 (asucc g a5))))) (ex_intro2 A (\lambda (a4: A).(eq A (AHead a1 a3) (AHead
-a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3 (refl_equal A
-(AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4)))) H2)))))))
-a)))).
+A).A) with [(ASort _ _) \Rightarrow a2 | (AHead _ a4) \Rightarrow a4]))
+(AHead a1 a2) (AHead a0 (asucc g a3)) H1) in (\lambda (H4: (eq A a1 a0)).(let
+H5 \def (eq_ind_r A a0 (\lambda (a4: A).((eq A (AHead a1 a2) (asucc g a4))
+\to (ex2 A (\lambda (a5: A).(eq A a4 (AHead a1 a5))) (\lambda (a5: A).(eq A
+a2 (asucc g a5)))))) H a1 H4) in (eq_ind A a1 (\lambda (a4: A).(ex2 A
+(\lambda (a5: A).(eq A (AHead a4 a3) (AHead a1 a5))) (\lambda (a5: A).(eq A
+a2 (asucc g a5))))) (let H6 \def (eq_ind A a2 (\lambda (a4: A).((eq A (AHead
+a1 a4) (asucc g a3)) \to (ex2 A (\lambda (a5: A).(eq A a3 (AHead a1 a5)))
+(\lambda (a5: A).(eq A a4 (asucc g a5)))))) H0 (asucc g a3) H3) in (let H7
+\def (eq_ind A a2 (\lambda (a4: A).((eq A (AHead a1 a4) (asucc g a1)) \to
+(ex2 A (\lambda (a5: A).(eq A a1 (AHead a1 a5))) (\lambda (a5: A).(eq A a4
+(asucc g a5)))))) H5 (asucc g a3) H3) in (eq_ind_r A (asucc g a3) (\lambda
+(a4: A).(ex2 A (\lambda (a5: A).(eq A (AHead a1 a3) (AHead a1 a5))) (\lambda
+(a5: A).(eq A a4 (asucc g a5))))) (ex_intro2 A (\lambda (a4: A).(eq A (AHead
+a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3
+(refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4))))
+H2))))))) a)))).