-\Rightarrow a4])) in (let TMP_40 \def (AHead a1 a2) in (let TMP_41 \def
-(asucc g a3) in (let TMP_42 \def (AHead a0 TMP_41) in (let H3 \def (f_equal A
-A TMP_39 TMP_40 TMP_42 H1) in (let TMP_85 \def (\lambda (H4: (eq A a1
-a0)).(let TMP_47 \def (\lambda (a4: A).((eq A (AHead a1 a2) (asucc g a4)) \to
-(let TMP_44 \def (\lambda (a5: A).(let TMP_43 \def (AHead a1 a5) in (eq A a4
-TMP_43))) in (let TMP_46 \def (\lambda (a5: A).(let TMP_45 \def (asucc g a5)
-in (eq A a2 TMP_45))) in (ex2 A TMP_44 TMP_46))))) in (let H5 \def (eq_ind_r
-A a0 TMP_47 H a1 H4) in (let TMP_53 \def (\lambda (a4: A).(let TMP_50 \def
-(\lambda (a5: A).(let TMP_48 \def (AHead a4 a3) in (let TMP_49 \def (AHead a1
-a5) in (eq A TMP_48 TMP_49)))) in (let TMP_52 \def (\lambda (a5: A).(let
-TMP_51 \def (asucc g a5) in (eq A a2 TMP_51))) in (ex2 A TMP_50 TMP_52)))) in
-(let TMP_58 \def (\lambda (a4: A).((eq A (AHead a1 a4) (asucc g a3)) \to (let
-TMP_55 \def (\lambda (a5: A).(let TMP_54 \def (AHead a1 a5) in (eq A a3
-TMP_54))) in (let TMP_57 \def (\lambda (a5: A).(let TMP_56 \def (asucc g a5)
-in (eq A a4 TMP_56))) in (ex2 A TMP_55 TMP_57))))) in (let TMP_59 \def (asucc
-g a3) in (let H6 \def (eq_ind A a2 TMP_58 H0 TMP_59 H3) in (let TMP_64 \def
-(\lambda (a4: A).((eq A (AHead a1 a4) (asucc g a1)) \to (let TMP_61 \def
-(\lambda (a5: A).(let TMP_60 \def (AHead a1 a5) in (eq A a1 TMP_60))) in (let
-TMP_63 \def (\lambda (a5: A).(let TMP_62 \def (asucc g a5) in (eq A a4
-TMP_62))) in (ex2 A TMP_61 TMP_63))))) in (let TMP_65 \def (asucc g a3) in
-(let H7 \def (eq_ind A a2 TMP_64 H5 TMP_65 H3) in (let TMP_66 \def (asucc g
-a3) in (let TMP_72 \def (\lambda (a4: A).(let TMP_69 \def (\lambda (a5:
-A).(let TMP_67 \def (AHead a1 a3) in (let TMP_68 \def (AHead a1 a5) in (eq A
-TMP_67 TMP_68)))) in (let TMP_71 \def (\lambda (a5: A).(let TMP_70 \def
-(asucc g a5) in (eq A a4 TMP_70))) in (ex2 A TMP_69 TMP_71)))) in (let TMP_75
-\def (\lambda (a4: A).(let TMP_73 \def (AHead a1 a3) in (let TMP_74 \def
-(AHead a1 a4) in (eq A TMP_73 TMP_74)))) in (let TMP_78 \def (\lambda (a4:
-A).(let TMP_76 \def (asucc g a3) in (let TMP_77 \def (asucc g a4) in (eq A
-TMP_76 TMP_77)))) in (let TMP_79 \def (AHead a1 a3) in (let TMP_80 \def
-(refl_equal A TMP_79) in (let TMP_81 \def (asucc g a3) in (let TMP_82 \def
-(refl_equal A TMP_81) in (let TMP_83 \def (ex_intro2 A TMP_75 TMP_78 a3
-TMP_80 TMP_82) in (let TMP_84 \def (eq_ind_r A TMP_66 TMP_72 TMP_83 a2 H3) in
-(eq_ind A a1 TMP_53 TMP_84 a0 H4))))))))))))))))))))) in (TMP_85
-H2))))))))))))))))) in (A_ind TMP_5 TMP_34 TMP_86 a))))))).
+\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)))).