-A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a1 |
-(AHead a4 _) \Rightarrow a4])) (AHead a1 a2) (AHead a0 (asucc g a3)) H1) in
-((let H3 \def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_:
-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)))).
-(* COMMENTS
-Initial nodes: 957
-END *)
+A).(match e with [(ASort _ _) \Rightarrow a1 | (AHead a4 _) \Rightarrow a4]))
+(AHead a1 a2) (AHead a0 (asucc g a3)) H1) in ((let H3 \def (f_equal A A
+(\lambda (e: A).(match e 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)))).