(* This file was automatically generated: do not edit *********************)
-include "Basic-1/ty3/arity_props.ma".
+include "basic_1/ty3/arity_props.ma".
-include "Basic-1/pc3/nf2.ma".
+include "basic_1/pc3/nf2.ma".
-include "Basic-1/nf2/fwd.ma".
+include "basic_1/nf2/fwd.ma".
theorem ty3_gen_appl_nf2:
\forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (v: T).(\forall (x:
T).(nf2 c (THead (Bind Abst) u t))))))))))
\def
\lambda (g: G).(\lambda (c: C).(\lambda (w: T).(\lambda (v: T).(\lambda (x:
-T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(ex3_2_ind T T (\lambda
-(u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t))
-x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (ex4_2 T T (\lambda (u:
-T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
-(\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
-T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x0: T).(\lambda (x1:
-T).(\lambda (H0: (pc3 c (THead (Flat Appl) w (THead (Bind Abst) x0 x1))
-x)).(\lambda (H1: (ty3 g c v (THead (Bind Abst) x0 x1))).(\lambda (H2: (ty3 g
-c w x0)).(let H_x \def (ty3_correct g c v (THead (Bind Abst) x0 x1) H1) in
-(let H3 \def H_x in (ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) x0
-x1) t)) (ex4_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl)
-w (THead (Bind Abst) u t)) x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v
-(THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3 g c w u)))
-(\lambda (u: T).(\lambda (t: T).(nf2 c (THead (Bind Abst) u t))))) (\lambda
-(x2: T).(\lambda (H4: (ty3 g c (THead (Bind Abst) x0 x1) x2)).(let H_x0 \def
-(ty3_correct g c w x0 H2) in (let H5 \def H_x0 in (ex_ind T (\lambda (t:
-T).(ty3 g c x0 t)) (ex4_2 T T (\lambda (u: T).(\lambda (t: T).(pc3 c (THead
-(Flat Appl) w (THead (Bind Abst) u t)) x))) (\lambda (u: T).(\lambda (t:
-T).(ty3 g c v (THead (Bind Abst) u t)))) (\lambda (u: T).(\lambda (_: T).(ty3
-g c w u))) (\lambda (u: T).(\lambda (t: T).(nf2 c (THead (Bind Abst) u t)))))
-(\lambda (x3: T).(\lambda (H6: (ty3 g c x0 x3)).(let H7 \def (ty3_sn3 g c
-(THead (Bind Abst) x0 x1) x2 H4) in (let H_x1 \def (nf2_sn3 c (THead (Bind
-Abst) x0 x1) H7) in (let H8 \def H_x1 in (ex2_ind T (\lambda (u: T).(pr3 c
-(THead (Bind Abst) x0 x1) u)) (\lambda (u: T).(nf2 c u)) (ex4_2 T T (\lambda
-(u: T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t))
-x))) (\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
-T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x4: T).(\lambda (H9: (pr3 c
-(THead (Bind Abst) x0 x1) x4)).(\lambda (H10: (nf2 c x4)).(let H11 \def
-(pr3_gen_abst c x0 x1 x4 H9) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t2:
-T).(eq T x4 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
-T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
-(u: T).(pr3 (CHead c (Bind b) u) x1 t2))))) (ex4_2 T T (\lambda (u:
-T).(\lambda (t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x)))
-(\lambda (u: T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t))))
-(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t:
-T).(nf2 c (THead (Bind Abst) u t))))) (\lambda (x5: T).(\lambda (x6:
-T).(\lambda (H12: (eq T x4 (THead (Bind Abst) x5 x6))).(\lambda (H13: (pr3 c
-x0 x5)).(\lambda (H14: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind
-b) u) x1 x6))))).(let H15 \def (eq_ind T x4 (\lambda (t: T).(nf2 c t)) H10
-(THead (Bind Abst) x5 x6) H12) in (let H16 \def (pr3_head_12 c x0 x5 H13
-(Bind Abst) x1 x6 (H14 Abst x5)) in (ex4_2_intro T T (\lambda (u: T).(\lambda
-(t: T).(pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x))) (\lambda (u:
-T).(\lambda (t: T).(ty3 g c v (THead (Bind Abst) u t)))) (\lambda (u:
-T).(\lambda (_: T).(ty3 g c w u))) (\lambda (u: T).(\lambda (t: T).(nf2 c
-(THead (Bind Abst) u t)))) x5 x6 (pc3_pr3_conf c (THead (Flat Appl) w (THead
-(Bind Abst) x0 x1)) x H0 (THead (Flat Appl) w (THead (Bind Abst) x5 x6))
-(pr3_thin_dx c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5 x6) H16 w
-Appl)) (ty3_conv g c (THead (Bind Abst) x5 x6) x2 (ty3_sred_pr3 c (THead
-(Bind Abst) x0 x1) (THead (Bind Abst) x5 x6) H16 g x2 H4) v (THead (Bind
-Abst) x0 x1) H1 (pc3_pr3_r c (THead (Bind Abst) x0 x1) (THead (Bind Abst) x5
-x6) H16)) (ty3_conv g c x5 x3 (ty3_sred_pr3 c x0 x5 H13 g x3 H6) w x0 H2
-(pc3_pr3_r c x0 x5 H13)) H15)))))))) H11))))) H8)))))) H5))))) H3))))))))
-(ty3_gen_appl g c w v x H))))))).
-(* COMMENTS
-Initial nodes: 1289
-END *)
+T).(\lambda (H: (ty3 g c (THead (Flat Appl) w v) x)).(let TMP_5 \def (\lambda
+(u: T).(\lambda (t: T).(let TMP_1 \def (Flat Appl) in (let TMP_2 \def (Bind
+Abst) in (let TMP_3 \def (THead TMP_2 u t) in (let TMP_4 \def (THead TMP_1 w
+TMP_3) in (pc3 c TMP_4 x))))))) in (let TMP_8 \def (\lambda (u: T).(\lambda
+(t: T).(let TMP_6 \def (Bind Abst) in (let TMP_7 \def (THead TMP_6 u t) in
+(ty3 g c v TMP_7))))) in (let TMP_9 \def (\lambda (u: T).(\lambda (_: T).(ty3
+g c w u))) in (let TMP_14 \def (\lambda (u: T).(\lambda (t: T).(let TMP_10
+\def (Flat Appl) in (let TMP_11 \def (Bind Abst) in (let TMP_12 \def (THead
+TMP_11 u t) in (let TMP_13 \def (THead TMP_10 w TMP_12) in (pc3 c TMP_13
+x))))))) in (let TMP_17 \def (\lambda (u: T).(\lambda (t: T).(let TMP_15 \def
+(Bind Abst) in (let TMP_16 \def (THead TMP_15 u t) in (ty3 g c v TMP_16)))))
+in (let TMP_18 \def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let
+TMP_21 \def (\lambda (u: T).(\lambda (t: T).(let TMP_19 \def (Bind Abst) in
+(let TMP_20 \def (THead TMP_19 u t) in (nf2 c TMP_20))))) in (let TMP_22 \def
+(ex4_2 T T TMP_14 TMP_17 TMP_18 TMP_21) in (let TMP_149 \def (\lambda (x0:
+T).(\lambda (x1: T).(\lambda (H0: (pc3 c (THead (Flat Appl) w (THead (Bind
+Abst) x0 x1)) x)).(\lambda (H1: (ty3 g c v (THead (Bind Abst) x0
+x1))).(\lambda (H2: (ty3 g c w x0)).(let TMP_23 \def (Bind Abst) in (let
+TMP_24 \def (THead TMP_23 x0 x1) in (let H_x \def (ty3_correct g c v TMP_24
+H1) in (let H3 \def H_x in (let TMP_27 \def (\lambda (t: T).(let TMP_25 \def
+(Bind Abst) in (let TMP_26 \def (THead TMP_25 x0 x1) in (ty3 g c TMP_26 t))))
+in (let TMP_32 \def (\lambda (u: T).(\lambda (t: T).(let TMP_28 \def (Flat
+Appl) in (let TMP_29 \def (Bind Abst) in (let TMP_30 \def (THead TMP_29 u t)
+in (let TMP_31 \def (THead TMP_28 w TMP_30) in (pc3 c TMP_31 x))))))) in (let
+TMP_35 \def (\lambda (u: T).(\lambda (t: T).(let TMP_33 \def (Bind Abst) in
+(let TMP_34 \def (THead TMP_33 u t) in (ty3 g c v TMP_34))))) in (let TMP_36
+\def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_39 \def
+(\lambda (u: T).(\lambda (t: T).(let TMP_37 \def (Bind Abst) in (let TMP_38
+\def (THead TMP_37 u t) in (nf2 c TMP_38))))) in (let TMP_40 \def (ex4_2 T T
+TMP_32 TMP_35 TMP_36 TMP_39) in (let TMP_148 \def (\lambda (x2: T).(\lambda
+(H4: (ty3 g c (THead (Bind Abst) x0 x1) x2)).(let H_x0 \def (ty3_correct g c
+w x0 H2) in (let H5 \def H_x0 in (let TMP_41 \def (\lambda (t: T).(ty3 g c x0
+t)) in (let TMP_46 \def (\lambda (u: T).(\lambda (t: T).(let TMP_42 \def
+(Flat Appl) in (let TMP_43 \def (Bind Abst) in (let TMP_44 \def (THead TMP_43
+u t) in (let TMP_45 \def (THead TMP_42 w TMP_44) in (pc3 c TMP_45 x))))))) in
+(let TMP_49 \def (\lambda (u: T).(\lambda (t: T).(let TMP_47 \def (Bind Abst)
+in (let TMP_48 \def (THead TMP_47 u t) in (ty3 g c v TMP_48))))) in (let
+TMP_50 \def (\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_53
+\def (\lambda (u: T).(\lambda (t: T).(let TMP_51 \def (Bind Abst) in (let
+TMP_52 \def (THead TMP_51 u t) in (nf2 c TMP_52))))) in (let TMP_54 \def
+(ex4_2 T T TMP_46 TMP_49 TMP_50 TMP_53) in (let TMP_147 \def (\lambda (x3:
+T).(\lambda (H6: (ty3 g c x0 x3)).(let TMP_55 \def (Bind Abst) in (let TMP_56
+\def (THead TMP_55 x0 x1) in (let H7 \def (ty3_sn3 g c TMP_56 x2 H4) in (let
+TMP_57 \def (Bind Abst) in (let TMP_58 \def (THead TMP_57 x0 x1) in (let H_x1
+\def (nf2_sn3 c TMP_58 H7) in (let H8 \def H_x1 in (let TMP_61 \def (\lambda
+(u: T).(let TMP_59 \def (Bind Abst) in (let TMP_60 \def (THead TMP_59 x0 x1)
+in (pr3 c TMP_60 u)))) in (let TMP_62 \def (\lambda (u: T).(nf2 c u)) in (let
+TMP_67 \def (\lambda (u: T).(\lambda (t: T).(let TMP_63 \def (Flat Appl) in
+(let TMP_64 \def (Bind Abst) in (let TMP_65 \def (THead TMP_64 u t) in (let
+TMP_66 \def (THead TMP_63 w TMP_65) in (pc3 c TMP_66 x))))))) in (let TMP_70
+\def (\lambda (u: T).(\lambda (t: T).(let TMP_68 \def (Bind Abst) in (let
+TMP_69 \def (THead TMP_68 u t) in (ty3 g c v TMP_69))))) in (let TMP_71 \def
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_74 \def (\lambda
+(u: T).(\lambda (t: T).(let TMP_72 \def (Bind Abst) in (let TMP_73 \def
+(THead TMP_72 u t) in (nf2 c TMP_73))))) in (let TMP_75 \def (ex4_2 T T
+TMP_67 TMP_70 TMP_71 TMP_74) in (let TMP_146 \def (\lambda (x4: T).(\lambda
+(H9: (pr3 c (THead (Bind Abst) x0 x1) x4)).(\lambda (H10: (nf2 c x4)).(let
+H11 \def (pr3_gen_abst c x0 x1 x4 H9) in (let TMP_78 \def (\lambda (u2:
+T).(\lambda (t2: T).(let TMP_76 \def (Bind Abst) in (let TMP_77 \def (THead
+TMP_76 u2 t2) in (eq T x4 TMP_77))))) in (let TMP_79 \def (\lambda (u2:
+T).(\lambda (_: T).(pr3 c x0 u2))) in (let TMP_82 \def (\lambda (_:
+T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(let TMP_80 \def (Bind b)
+in (let TMP_81 \def (CHead c TMP_80 u) in (pr3 TMP_81 x1 t2))))))) in (let
+TMP_87 \def (\lambda (u: T).(\lambda (t: T).(let TMP_83 \def (Flat Appl) in
+(let TMP_84 \def (Bind Abst) in (let TMP_85 \def (THead TMP_84 u t) in (let
+TMP_86 \def (THead TMP_83 w TMP_85) in (pc3 c TMP_86 x))))))) in (let TMP_90
+\def (\lambda (u: T).(\lambda (t: T).(let TMP_88 \def (Bind Abst) in (let
+TMP_89 \def (THead TMP_88 u t) in (ty3 g c v TMP_89))))) in (let TMP_91 \def
+(\lambda (u: T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_94 \def (\lambda
+(u: T).(\lambda (t: T).(let TMP_92 \def (Bind Abst) in (let TMP_93 \def
+(THead TMP_92 u t) in (nf2 c TMP_93))))) in (let TMP_95 \def (ex4_2 T T
+TMP_87 TMP_90 TMP_91 TMP_94) in (let TMP_145 \def (\lambda (x5: T).(\lambda
+(x6: T).(\lambda (H12: (eq T x4 (THead (Bind Abst) x5 x6))).(\lambda (H13:
+(pr3 c x0 x5)).(\lambda (H14: ((\forall (b: B).(\forall (u: T).(pr3 (CHead c
+(Bind b) u) x1 x6))))).(let TMP_96 \def (\lambda (t: T).(nf2 c t)) in (let
+TMP_97 \def (Bind Abst) in (let TMP_98 \def (THead TMP_97 x5 x6) in (let H15
+\def (eq_ind T x4 TMP_96 H10 TMP_98 H12) in (let TMP_99 \def (Bind Abst) in
+(let TMP_100 \def (H14 Abst x5) in (let H16 \def (pr3_head_12 c x0 x5 H13
+TMP_99 x1 x6 TMP_100) in (let TMP_105 \def (\lambda (u: T).(\lambda (t:
+T).(let TMP_101 \def (Flat Appl) in (let TMP_102 \def (Bind Abst) in (let
+TMP_103 \def (THead TMP_102 u t) in (let TMP_104 \def (THead TMP_101 w
+TMP_103) in (pc3 c TMP_104 x))))))) in (let TMP_108 \def (\lambda (u:
+T).(\lambda (t: T).(let TMP_106 \def (Bind Abst) in (let TMP_107 \def (THead
+TMP_106 u t) in (ty3 g c v TMP_107))))) in (let TMP_109 \def (\lambda (u:
+T).(\lambda (_: T).(ty3 g c w u))) in (let TMP_112 \def (\lambda (u:
+T).(\lambda (t: T).(let TMP_110 \def (Bind Abst) in (let TMP_111 \def (THead
+TMP_110 u t) in (nf2 c TMP_111))))) in (let TMP_113 \def (Flat Appl) in (let
+TMP_114 \def (Bind Abst) in (let TMP_115 \def (THead TMP_114 x0 x1) in (let
+TMP_116 \def (THead TMP_113 w TMP_115) in (let TMP_117 \def (Flat Appl) in
+(let TMP_118 \def (Bind Abst) in (let TMP_119 \def (THead TMP_118 x5 x6) in
+(let TMP_120 \def (THead TMP_117 w TMP_119) in (let TMP_121 \def (Bind Abst)
+in (let TMP_122 \def (THead TMP_121 x0 x1) in (let TMP_123 \def (Bind Abst)
+in (let TMP_124 \def (THead TMP_123 x5 x6) in (let TMP_125 \def (pr3_thin_dx
+c TMP_122 TMP_124 H16 w Appl) in (let TMP_126 \def (pc3_pr3_conf c TMP_116 x
+H0 TMP_120 TMP_125) in (let TMP_127 \def (Bind Abst) in (let TMP_128 \def
+(THead TMP_127 x5 x6) in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def
+(THead TMP_129 x0 x1) in (let TMP_131 \def (Bind Abst) in (let TMP_132 \def
+(THead TMP_131 x5 x6) in (let TMP_133 \def (ty3_sred_pr3 c TMP_130 TMP_132
+H16 g x2 H4) in (let TMP_134 \def (Bind Abst) in (let TMP_135 \def (THead
+TMP_134 x0 x1) in (let TMP_136 \def (Bind Abst) in (let TMP_137 \def (THead
+TMP_136 x0 x1) in (let TMP_138 \def (Bind Abst) in (let TMP_139 \def (THead
+TMP_138 x5 x6) in (let TMP_140 \def (pc3_pr3_r c TMP_137 TMP_139 H16) in (let
+TMP_141 \def (ty3_conv g c TMP_128 x2 TMP_133 v TMP_135 H1 TMP_140) in (let
+TMP_142 \def (ty3_sred_pr3 c x0 x5 H13 g x3 H6) in (let TMP_143 \def
+(pc3_pr3_r c x0 x5 H13) in (let TMP_144 \def (ty3_conv g c x5 x3 TMP_142 w x0
+H2 TMP_143) in (ex4_2_intro T T TMP_105 TMP_108 TMP_109 TMP_112 x5 x6 TMP_126
+TMP_141 TMP_144 H15))))))))))))))))))))))))))))))))))))))))))))))))) in
+(ex3_2_ind T T TMP_78 TMP_79 TMP_82 TMP_95 TMP_145 H11)))))))))))))) in
+(ex2_ind T TMP_61 TMP_62 TMP_75 TMP_146 H8)))))))))))))))))) in (ex_ind T
+TMP_41 TMP_54 TMP_147 H5)))))))))))) in (ex_ind T TMP_27 TMP_40 TMP_148
+H3))))))))))))))))) in (let TMP_150 \def (ty3_gen_appl g c w v x H) in
+(ex3_2_ind T T TMP_5 TMP_8 TMP_9 TMP_22 TMP_149 TMP_150)))))))))))))))).
theorem ty3_inv_lref_nf2_pc3:
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (i: nat).((ty3 g c
((pc3 c u1 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))))
\def
\lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (i: nat).(\lambda
-(H: (ty3 g c (TLRef i) u1)).(insert_eq T (TLRef i) (\lambda (t: T).(ty3 g c t
-u1)) (\lambda (t: T).((nf2 c t) \to (\forall (u2: T).((nf2 c u2) \to ((pc3 c
-u1 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))) (\lambda
-(y: T).(\lambda (H0: (ty3 g c y u1)).(ty3_ind g (\lambda (c0: C).(\lambda (t:
-T).(\lambda (t0: T).((eq T t (TLRef i)) \to ((nf2 c0 t) \to (\forall (u2:
-T).((nf2 c0 u2) \to ((pc3 c0 t0 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift
-(S i) O u)))))))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t:
-T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2 (TLRef i)) \to ((nf2
-c0 t2) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t u2) \to (ex T
-(\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda (u: T).(\lambda
-(t1: T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T u (TLRef i)) \to
-((nf2 c0 u) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t1 u2) \to (ex T
-(\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (H5: (pc3 c0
-t1 t2)).(\lambda (H6: (eq T u (TLRef i))).(\lambda (H7: (nf2 c0 u)).(\lambda
-(u2: T).(\lambda (H8: (nf2 c0 u2)).(\lambda (H9: (pc3 c0 t2 u2)).(let H10
-\def (eq_ind T u (\lambda (t0: T).(nf2 c0 t0)) H7 (TLRef i) H6) in (let H11
-\def (eq_ind T u (\lambda (t0: T).((eq T t0 (TLRef i)) \to ((nf2 c0 t0) \to
-(\forall (u3: T).((nf2 c0 u3) \to ((pc3 c0 t1 u3) \to (ex T (\lambda (u0:
-T).(eq T u3 (lift (S i) O u0)))))))))) H4 (TLRef i) H6) in (let H12 \def
-(eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t1)) H3 (TLRef i) H6) in (let H_y
-\def (H11 (refl_equal T (TLRef i)) H10 u2 H8) in (H_y (pc3_t t2 c0 t1 H5 u2
-H9))))))))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (H1: (eq
-T (TSort m) (TLRef i))).(\lambda (_: (nf2 c0 (TSort m))).(\lambda (u2:
-T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (TSort (next g m))
-u2)).(let H5 \def (eq_ind T (TSort m) (\lambda (ee: T).(match ee in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef i) H1) in
-(False_ind (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u)))) H5)))))))))
-(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
-(H1: (getl n c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g
-d u t)).(\lambda (_: (((eq T u (TLRef i)) \to ((nf2 d u) \to (\forall (u2:
-T).((nf2 d u2) \to ((pc3 d t u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S
-i) O u0))))))))))).(\lambda (H4: (eq T (TLRef n) (TLRef i))).(\lambda (H5:
-(nf2 c0 (TLRef n))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (H7:
-(pc3 c0 (lift (S n) O t) u2)).(let H8 \def (f_equal T nat (\lambda (e:
-T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
-(TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef
-i) H4) in (let H9 \def (eq_ind nat n (\lambda (n0: nat).(pc3 c0 (lift (S n0)
-O t) u2)) H7 i H8) in (let H10 \def (eq_ind nat n (\lambda (n0: nat).(nf2 c0
-(TLRef n0))) H5 i H8) in (let H11 \def (eq_ind nat n (\lambda (n0: nat).(getl
-n0 c0 (CHead d (Bind Abbr) u))) H1 i H8) in (nf2_gen_lref c0 d u i H11 H10
-(ex T (\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))))))))))))))
+(H: (ty3 g c (TLRef i) u1)).(let TMP_1 \def (TLRef i) in (let TMP_2 \def
+(\lambda (t: T).(ty3 g c t u1)) in (let TMP_6 \def (\lambda (t: T).((nf2 c t)
+\to (\forall (u2: T).((nf2 c u2) \to ((pc3 c u1 u2) \to (let TMP_5 \def
+(\lambda (u: T).(let TMP_3 \def (S i) in (let TMP_4 \def (lift TMP_3 O u) in
+(eq T u2 TMP_4)))) in (ex T TMP_5))))))) in (let TMP_115 \def (\lambda (y:
+T).(\lambda (H0: (ty3 g c y u1)).(let TMP_10 \def (\lambda (c0: C).(\lambda
+(t: T).(\lambda (t0: T).((eq T t (TLRef i)) \to ((nf2 c0 t) \to (\forall (u2:
+T).((nf2 c0 u2) \to ((pc3 c0 t0 u2) \to (let TMP_9 \def (\lambda (u: T).(let
+TMP_7 \def (S i) in (let TMP_8 \def (lift TMP_7 O u) in (eq T u2 TMP_8)))) in
+(ex T TMP_9)))))))))) in (let TMP_23 \def (\lambda (c0: C).(\lambda (t2:
+T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: (((eq T t2
+(TLRef i)) \to ((nf2 c0 t2) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t
+u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda
+(u: T).(\lambda (t1: T).(\lambda (H3: (ty3 g c0 u t1)).(\lambda (H4: (((eq T
+u (TLRef i)) \to ((nf2 c0 u) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0
+t1 u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
+u0))))))))))).(\lambda (H5: (pc3 c0 t1 t2)).(\lambda (H6: (eq T u (TLRef
+i))).(\lambda (H7: (nf2 c0 u)).(\lambda (u2: T).(\lambda (H8: (nf2 c0
+u2)).(\lambda (H9: (pc3 c0 t2 u2)).(let TMP_11 \def (\lambda (t0: T).(nf2 c0
+t0)) in (let TMP_12 \def (TLRef i) in (let H10 \def (eq_ind T u TMP_11 H7
+TMP_12 H6) in (let TMP_16 \def (\lambda (t0: T).((eq T t0 (TLRef i)) \to
+((nf2 c0 t0) \to (\forall (u3: T).((nf2 c0 u3) \to ((pc3 c0 t1 u3) \to (let
+TMP_15 \def (\lambda (u0: T).(let TMP_13 \def (S i) in (let TMP_14 \def (lift
+TMP_13 O u0) in (eq T u3 TMP_14)))) in (ex T TMP_15)))))))) in (let TMP_17
+\def (TLRef i) in (let H11 \def (eq_ind T u TMP_16 H4 TMP_17 H6) in (let
+TMP_18 \def (\lambda (t0: T).(ty3 g c0 t0 t1)) in (let TMP_19 \def (TLRef i)
+in (let H12 \def (eq_ind T u TMP_18 H3 TMP_19 H6) in (let TMP_20 \def (TLRef
+i) in (let TMP_21 \def (refl_equal T TMP_20) in (let H_y \def (H11 TMP_21 H10
+u2 H8) in (let TMP_22 \def (pc3_t t2 c0 t1 H5 u2 H9) in (H_y
+TMP_22))))))))))))))))))))))))))))) in (let TMP_31 \def (\lambda (c0:
+C).(\lambda (m: nat).(\lambda (H1: (eq T (TSort m) (TLRef i))).(\lambda (_:
+(nf2 c0 (TSort m))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_:
+(pc3 c0 (TSort (next g m)) u2)).(let TMP_24 \def (TSort m) in (let TMP_25
+\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow True | (TLRef _)
+\Rightarrow False | (THead _ _ _) \Rightarrow False])) in (let TMP_26 \def
+(TLRef i) in (let H5 \def (eq_ind T TMP_24 TMP_25 I TMP_26 H1) in (let TMP_29
+\def (\lambda (u: T).(let TMP_27 \def (S i) in (let TMP_28 \def (lift TMP_27
+O u) in (eq T u2 TMP_28)))) in (let TMP_30 \def (ex T TMP_29) in (False_ind
+TMP_30 H5)))))))))))))) in (let TMP_47 \def (\lambda (n: nat).(\lambda (c0:
+C).(\lambda (d: C).(\lambda (u: T).(\lambda (H1: (getl n c0 (CHead d (Bind
+Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (_: (((eq T u
+(TLRef i)) \to ((nf2 d u) \to (\forall (u2: T).((nf2 d u2) \to ((pc3 d t u2)
+\to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (H4:
+(eq T (TLRef n) (TLRef i))).(\lambda (H5: (nf2 c0 (TLRef n))).(\lambda (u2:
+T).(\lambda (_: (nf2 c0 u2)).(\lambda (H7: (pc3 c0 (lift (S n) O t) u2)).(let
+TMP_32 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow n | (TLRef
+n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow n])) in (let TMP_33 \def
+(TLRef n) in (let TMP_34 \def (TLRef i) in (let H8 \def (f_equal T nat TMP_32
+TMP_33 TMP_34 H4) in (let TMP_37 \def (\lambda (n0: nat).(let TMP_35 \def (S
+n0) in (let TMP_36 \def (lift TMP_35 O t) in (pc3 c0 TMP_36 u2)))) in (let H9
+\def (eq_ind nat n TMP_37 H7 i H8) in (let TMP_39 \def (\lambda (n0:
+nat).(let TMP_38 \def (TLRef n0) in (nf2 c0 TMP_38))) in (let H10 \def
+(eq_ind nat n TMP_39 H5 i H8) in (let TMP_42 \def (\lambda (n0: nat).(let
+TMP_40 \def (Bind Abbr) in (let TMP_41 \def (CHead d TMP_40 u) in (getl n0 c0
+TMP_41)))) in (let H11 \def (eq_ind nat n TMP_42 H1 i H8) in (let TMP_45 \def
+(\lambda (u0: T).(let TMP_43 \def (S i) in (let TMP_44 \def (lift TMP_43 O
+u0) in (eq T u2 TMP_44)))) in (let TMP_46 \def (ex T TMP_45) in (nf2_gen_lref
+c0 d u i H11 H10 TMP_46)))))))))))))))))))))))))) in (let TMP_87 \def
(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
(H1: (getl n c0 (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (_: (ty3 g
d u t)).(\lambda (_: (((eq T u (TLRef i)) \to ((nf2 d u) \to (\forall (u2:
T).((nf2 d u2) \to ((pc3 d t u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S
i) O u0))))))))))).(\lambda (H4: (eq T (TLRef n) (TLRef i))).(\lambda (H5:
(nf2 c0 (TLRef n))).(\lambda (u2: T).(\lambda (H6: (nf2 c0 u2)).(\lambda (H7:
-(pc3 c0 (lift (S n) O u) u2)).(let H8 \def (f_equal T nat (\lambda (e:
-T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
-(TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef
-i) H4) in (let H9 \def (eq_ind nat n (\lambda (n0: nat).(pc3 c0 (lift (S n0)
-O u) u2)) H7 i H8) in (let H10 \def (eq_ind nat n (\lambda (n0: nat).(nf2 c0
-(TLRef n0))) H5 i H8) in (let H11 \def (eq_ind nat n (\lambda (n0: nat).(getl
-n0 c0 (CHead d (Bind Abst) u))) H1 i H8) in (let H_y \def (pc3_nf2_unfold c0
-(lift (S i) O u) u2 H9 H6) in (let H12 \def (pr3_gen_lift c0 u u2 (S i) O H_y
-d (getl_drop Abst c0 d u i H11)) in (ex2_ind T (\lambda (t2: T).(eq T u2
-(lift (S i) O t2))) (\lambda (t2: T).(pr3 d u t2)) (ex T (\lambda (u0: T).(eq
-T u2 (lift (S i) O u0)))) (\lambda (x: T).(\lambda (H13: (eq T u2 (lift (S i)
-O x))).(\lambda (_: (pr3 d u x)).(eq_ind_r T (lift (S i) O x) (\lambda (t0:
-T).(ex T (\lambda (u0: T).(eq T t0 (lift (S i) O u0))))) (ex_intro T (\lambda
-(u0: T).(eq T (lift (S i) O x) (lift (S i) O u0))) x (refl_equal T (lift (S
-i) O x))) u2 H13)))) H12)))))))))))))))))))) (\lambda (c0: C).(\lambda (u:
-T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (_: (((eq T u (TLRef
-i)) \to ((nf2 c0 u) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t u2) \to
-(ex T (\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (b:
-B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b)
-u) t1 t2)).(\lambda (_: (((eq T t1 (TLRef i)) \to ((nf2 (CHead c0 (Bind b) u)
-t1) \to (\forall (u2: T).((nf2 (CHead c0 (Bind b) u) u2) \to ((pc3 (CHead c0
-(Bind b) u) t2 u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
-u0))))))))))).(\lambda (H5: (eq T (THead (Bind b) u t1) (TLRef i))).(\lambda
-(_: (nf2 c0 (THead (Bind b) u t1))).(\lambda (u2: T).(\lambda (_: (nf2 c0
-u2)).(\lambda (_: (pc3 c0 (THead (Bind b) u t2) u2)).(let H9 \def (eq_ind T
-(THead (Bind b) u t1) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T
-(\lambda (u0: T).(eq T u2 (lift (S i) O u0)))) H9))))))))))))))))) (\lambda
-(c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c0 w u)).(\lambda
-(_: (((eq T w (TLRef i)) \to ((nf2 c0 w) \to (\forall (u2: T).((nf2 c0 u2)
-\to ((pc3 c0 u u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
-u0))))))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead
-(Bind Abst) u t))).(\lambda (_: (((eq T v (TLRef i)) \to ((nf2 c0 v) \to
-(\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 (THead (Bind Abst) u t) u2) \to
-(ex T (\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (H5: (eq
-T (THead (Flat Appl) w v) (TLRef i))).(\lambda (_: (nf2 c0 (THead (Flat Appl)
-w v))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead
-(Flat Appl) w (THead (Bind Abst) u t)) u2)).(let H9 \def (eq_ind T (THead
-(Flat Appl) w v) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
-_) \Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u0:
-T).(eq T u2 (lift (S i) O u0)))) H9)))))))))))))))) (\lambda (c0: C).(\lambda
-(t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda (_: (((eq T
-t1 (TLRef i)) \to ((nf2 c0 t1) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0
-t2 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda
-(t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (_: (((eq T t2 (TLRef i)) \to
-((nf2 c0 t2) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 t0 u2) \to (ex T
-(\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))).(\lambda (H5: (eq T
-(THead (Flat Cast) t2 t1) (TLRef i))).(\lambda (_: (nf2 c0 (THead (Flat Cast)
-t2 t1))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0
-(THead (Flat Cast) t0 t2) u2)).(let H9 \def (eq_ind T (THead (Flat Cast) t2
-t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
-_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
-\Rightarrow True])) I (TLRef i) H5) in (False_ind (ex T (\lambda (u: T).(eq T
-u2 (lift (S i) O u)))) H9))))))))))))))) c y u1 H0))) H))))).
-(* COMMENTS
-Initial nodes: 2175
-END *)
+(pc3 c0 (lift (S n) O u) u2)).(let TMP_48 \def (\lambda (e: T).(match e with
+[(TSort _) \Rightarrow n | (TLRef n0) \Rightarrow n0 | (THead _ _ _)
+\Rightarrow n])) in (let TMP_49 \def (TLRef n) in (let TMP_50 \def (TLRef i)
+in (let H8 \def (f_equal T nat TMP_48 TMP_49 TMP_50 H4) in (let TMP_53 \def
+(\lambda (n0: nat).(let TMP_51 \def (S n0) in (let TMP_52 \def (lift TMP_51 O
+u) in (pc3 c0 TMP_52 u2)))) in (let H9 \def (eq_ind nat n TMP_53 H7 i H8) in
+(let TMP_55 \def (\lambda (n0: nat).(let TMP_54 \def (TLRef n0) in (nf2 c0
+TMP_54))) in (let H10 \def (eq_ind nat n TMP_55 H5 i H8) in (let TMP_58 \def
+(\lambda (n0: nat).(let TMP_56 \def (Bind Abst) in (let TMP_57 \def (CHead d
+TMP_56 u) in (getl n0 c0 TMP_57)))) in (let H11 \def (eq_ind nat n TMP_58 H1
+i H8) in (let TMP_59 \def (S i) in (let TMP_60 \def (lift TMP_59 O u) in (let
+H_y \def (pc3_nf2_unfold c0 TMP_60 u2 H9 H6) in (let TMP_61 \def (S i) in
+(let TMP_62 \def (getl_drop Abst c0 d u i H11) in (let H12 \def (pr3_gen_lift
+c0 u u2 TMP_61 O H_y d TMP_62) in (let TMP_65 \def (\lambda (t2: T).(let
+TMP_63 \def (S i) in (let TMP_64 \def (lift TMP_63 O t2) in (eq T u2
+TMP_64)))) in (let TMP_66 \def (\lambda (t2: T).(pr3 d u t2)) in (let TMP_69
+\def (\lambda (u0: T).(let TMP_67 \def (S i) in (let TMP_68 \def (lift TMP_67
+O u0) in (eq T u2 TMP_68)))) in (let TMP_70 \def (ex T TMP_69) in (let TMP_86
+\def (\lambda (x: T).(\lambda (H13: (eq T u2 (lift (S i) O x))).(\lambda (_:
+(pr3 d u x)).(let TMP_71 \def (S i) in (let TMP_72 \def (lift TMP_71 O x) in
+(let TMP_76 \def (\lambda (t0: T).(let TMP_75 \def (\lambda (u0: T).(let
+TMP_73 \def (S i) in (let TMP_74 \def (lift TMP_73 O u0) in (eq T t0
+TMP_74)))) in (ex T TMP_75))) in (let TMP_81 \def (\lambda (u0: T).(let
+TMP_77 \def (S i) in (let TMP_78 \def (lift TMP_77 O x) in (let TMP_79 \def
+(S i) in (let TMP_80 \def (lift TMP_79 O u0) in (eq T TMP_78 TMP_80)))))) in
+(let TMP_82 \def (S i) in (let TMP_83 \def (lift TMP_82 O x) in (let TMP_84
+\def (refl_equal T TMP_83) in (let TMP_85 \def (ex_intro T TMP_81 x TMP_84)
+in (eq_ind_r T TMP_72 TMP_76 TMP_85 u2 H13)))))))))))) in (ex2_ind T TMP_65
+TMP_66 TMP_70 TMP_86 H12))))))))))))))))))))))))))))))))))) in (let TMP_96
+\def (\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0
+u t)).(\lambda (_: (((eq T u (TLRef i)) \to ((nf2 c0 u) \to (\forall (u2:
+T).((nf2 c0 u2) \to ((pc3 c0 t u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift
+(S i) O u0))))))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda (t2:
+T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t1 t2)).(\lambda (_: (((eq T t1
+(TLRef i)) \to ((nf2 (CHead c0 (Bind b) u) t1) \to (\forall (u2: T).((nf2
+(CHead c0 (Bind b) u) u2) \to ((pc3 (CHead c0 (Bind b) u) t2 u2) \to (ex T
+(\lambda (u0: T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (H5: (eq T
+(THead (Bind b) u t1) (TLRef i))).(\lambda (_: (nf2 c0 (THead (Bind b) u
+t1))).(\lambda (u2: T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead
+(Bind b) u t2) u2)).(let TMP_88 \def (Bind b) in (let TMP_89 \def (THead
+TMP_88 u t1) in (let TMP_90 \def (\lambda (ee: T).(match ee with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
+True])) in (let TMP_91 \def (TLRef i) in (let H9 \def (eq_ind T TMP_89 TMP_90
+I TMP_91 H5) in (let TMP_94 \def (\lambda (u0: T).(let TMP_92 \def (S i) in
+(let TMP_93 \def (lift TMP_92 O u0) in (eq T u2 TMP_93)))) in (let TMP_95
+\def (ex T TMP_94) in (False_ind TMP_95 H9))))))))))))))))))))))) in (let
+TMP_105 \def (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_:
+(ty3 g c0 w u)).(\lambda (_: (((eq T w (TLRef i)) \to ((nf2 c0 w) \to
+(\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0 u u2) \to (ex T (\lambda (u0:
+T).(eq T u2 (lift (S i) O u0))))))))))).(\lambda (v: T).(\lambda (t:
+T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (_: (((eq T v
+(TLRef i)) \to ((nf2 c0 v) \to (\forall (u2: T).((nf2 c0 u2) \to ((pc3 c0
+(THead (Bind Abst) u t) u2) \to (ex T (\lambda (u0: T).(eq T u2 (lift (S i) O
+u0))))))))))).(\lambda (H5: (eq T (THead (Flat Appl) w v) (TLRef
+i))).(\lambda (_: (nf2 c0 (THead (Flat Appl) w v))).(\lambda (u2: T).(\lambda
+(_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst)
+u t)) u2)).(let TMP_97 \def (Flat Appl) in (let TMP_98 \def (THead TMP_97 w
+v) in (let TMP_99 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in
+(let TMP_100 \def (TLRef i) in (let H9 \def (eq_ind T TMP_98 TMP_99 I TMP_100
+H5) in (let TMP_103 \def (\lambda (u0: T).(let TMP_101 \def (S i) in (let
+TMP_102 \def (lift TMP_101 O u0) in (eq T u2 TMP_102)))) in (let TMP_104 \def
+(ex T TMP_103) in (False_ind TMP_104 H9)))))))))))))))))))))) in (let TMP_114
+\def (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g
+c0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef i)) \to ((nf2 c0 t1) \to (\forall
+(u2: T).((nf2 c0 u2) \to ((pc3 c0 t2 u2) \to (ex T (\lambda (u: T).(eq T u2
+(lift (S i) O u))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2
+t0)).(\lambda (_: (((eq T t2 (TLRef i)) \to ((nf2 c0 t2) \to (\forall (u2:
+T).((nf2 c0 u2) \to ((pc3 c0 t0 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift
+(S i) O u))))))))))).(\lambda (H5: (eq T (THead (Flat Cast) t2 t1) (TLRef
+i))).(\lambda (_: (nf2 c0 (THead (Flat Cast) t2 t1))).(\lambda (u2:
+T).(\lambda (_: (nf2 c0 u2)).(\lambda (_: (pc3 c0 (THead (Flat Cast) t0 t2)
+u2)).(let TMP_106 \def (Flat Cast) in (let TMP_107 \def (THead TMP_106 t2 t1)
+in (let TMP_108 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
+False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in
+(let TMP_109 \def (TLRef i) in (let H9 \def (eq_ind T TMP_107 TMP_108 I
+TMP_109 H5) in (let TMP_112 \def (\lambda (u: T).(let TMP_110 \def (S i) in
+(let TMP_111 \def (lift TMP_110 O u) in (eq T u2 TMP_111)))) in (let TMP_113
+\def (ex T TMP_112) in (False_ind TMP_113 H9))))))))))))))))))))) in (ty3_ind
+g TMP_10 TMP_23 TMP_31 TMP_47 TMP_87 TMP_96 TMP_105 TMP_114 c y u1
+H0))))))))))) in (insert_eq T TMP_1 TMP_2 TMP_6 TMP_115 H))))))))).
theorem ty3_inv_lref_nf2:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (i: nat).((ty3 g c
\def
\lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
(H: (ty3 g c (TLRef i) u)).(\lambda (H0: (nf2 c (TLRef i))).(\lambda (H1:
-(nf2 c u)).(ty3_inv_lref_nf2_pc3 g c u i H H0 u H1 (pc3_refl c u)))))))).
-(* COMMENTS
-Initial nodes: 57
-END *)
+(nf2 c u)).(let TMP_1 \def (pc3_refl c u) in (ty3_inv_lref_nf2_pc3 g c u i H
+H0 u H1 TMP_1)))))))).
theorem ty3_inv_appls_lref_nf2:
\forall (g: G).(\forall (c: C).(\forall (vs: TList).(\forall (u1:
i) O u))) (\lambda (u: T).(pc3 c (THeads (Flat Appl) vs (lift (S i) O u))
u1))))))))))
\def
- \lambda (g: G).(\lambda (c: C).(\lambda (vs: TList).(TList_ind (\lambda (t:
-TList).(\forall (u1: T).(\forall (i: nat).((ty3 g c (THeads (Flat Appl) t
-(TLRef i)) u1) \to ((nf2 c (TLRef i)) \to ((nf2 c u1) \to (ex2 T (\lambda (u:
-T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3 c (THeads (Flat Appl) t
-(lift (S i) O u)) u1))))))))) (\lambda (u1: T).(\lambda (i: nat).(\lambda (H:
-(ty3 g c (TLRef i) u1)).(\lambda (H0: (nf2 c (TLRef i))).(\lambda (H1: (nf2 c
-u1)).(let H_x \def (ty3_inv_lref_nf2 g c u1 i H H0 H1) in (let H2 \def H_x in
-(ex_ind T (\lambda (u0: T).(eq T u1 (lift (S i) O u0))) (ex2 T (\lambda (u:
-T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3 c (lift (S i) O u) u1)))
-(\lambda (x: T).(\lambda (H3: (eq T u1 (lift (S i) O x))).(let H4 \def
-(eq_ind T u1 (\lambda (t: T).(nf2 c t)) H1 (lift (S i) O x) H3) in (eq_ind_r
-T (lift (S i) O x) (\lambda (t: T).(ex2 T (\lambda (u: T).(nf2 c (lift (S i)
-O u))) (\lambda (u: T).(pc3 c (lift (S i) O u) t)))) (ex_intro2 T (\lambda
-(u: T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3 c (lift (S i) O u)
-(lift (S i) O x))) x H4 (pc3_refl c (lift (S i) O x))) u1 H3)))) H2))))))))
-(\lambda (t: T).(\lambda (t0: TList).(\lambda (H: ((\forall (u1: T).(\forall
-(i: nat).((ty3 g c (THeads (Flat Appl) t0 (TLRef i)) u1) \to ((nf2 c (TLRef
-i)) \to ((nf2 c u1) \to (ex2 T (\lambda (u: T).(nf2 c (lift (S i) O u)))
-(\lambda (u: T).(pc3 c (THeads (Flat Appl) t0 (lift (S i) O u))
-u1)))))))))).(\lambda (u1: T).(\lambda (i: nat).(\lambda (H0: (ty3 g c (THead
-(Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) u1)).(\lambda (H1: (nf2 c
-(TLRef i))).(\lambda (_: (nf2 c u1)).(let H_x \def (ty3_gen_appl_nf2 g c t
-(THeads (Flat Appl) t0 (TLRef i)) u1 H0) in (let H3 \def H_x in (ex4_2_ind T
-T (\lambda (u: T).(\lambda (t1: T).(pc3 c (THead (Flat Appl) t (THead (Bind
-Abst) u t1)) u1))) (\lambda (u: T).(\lambda (t1: T).(ty3 g c (THeads (Flat
-Appl) t0 (TLRef i)) (THead (Bind Abst) u t1)))) (\lambda (u: T).(\lambda (_:
-T).(ty3 g c t u))) (\lambda (u: T).(\lambda (t1: T).(nf2 c (THead (Bind Abst)
-u t1)))) (ex2 T (\lambda (u: T).(nf2 c (lift (S i) O u))) (\lambda (u:
-T).(pc3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u)))
-u1))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (pc3 c (THead (Flat
+ \lambda (g: G).(\lambda (c: C).(\lambda (vs: TList).(let TMP_9 \def (\lambda
+(t: TList).(\forall (u1: T).(\forall (i: nat).((ty3 g c (THeads (Flat Appl) t
+(TLRef i)) u1) \to ((nf2 c (TLRef i)) \to ((nf2 c u1) \to (let TMP_3 \def
+(\lambda (u: T).(let TMP_1 \def (S i) in (let TMP_2 \def (lift TMP_1 O u) in
+(nf2 c TMP_2)))) in (let TMP_8 \def (\lambda (u: T).(let TMP_4 \def (Flat
+Appl) in (let TMP_5 \def (S i) in (let TMP_6 \def (lift TMP_5 O u) in (let
+TMP_7 \def (THeads TMP_4 t TMP_6) in (pc3 c TMP_7 u1)))))) in (ex2 T TMP_3
+TMP_8))))))))) in (let TMP_45 \def (\lambda (u1: T).(\lambda (i:
+nat).(\lambda (H: (ty3 g c (TLRef i) u1)).(\lambda (H0: (nf2 c (TLRef
+i))).(\lambda (H1: (nf2 c u1)).(let H_x \def (ty3_inv_lref_nf2 g c u1 i H H0
+H1) in (let H2 \def H_x in (let TMP_12 \def (\lambda (u0: T).(let TMP_10 \def
+(S i) in (let TMP_11 \def (lift TMP_10 O u0) in (eq T u1 TMP_11)))) in (let
+TMP_15 \def (\lambda (u: T).(let TMP_13 \def (S i) in (let TMP_14 \def (lift
+TMP_13 O u) in (nf2 c TMP_14)))) in (let TMP_18 \def (\lambda (u: T).(let
+TMP_16 \def (S i) in (let TMP_17 \def (lift TMP_16 O u) in (pc3 c TMP_17
+u1)))) in (let TMP_19 \def (ex2 T TMP_15 TMP_18) in (let TMP_44 \def (\lambda
+(x: T).(\lambda (H3: (eq T u1 (lift (S i) O x))).(let TMP_20 \def (\lambda
+(t: T).(nf2 c t)) in (let TMP_21 \def (S i) in (let TMP_22 \def (lift TMP_21
+O x) in (let H4 \def (eq_ind T u1 TMP_20 H1 TMP_22 H3) in (let TMP_23 \def (S
+i) in (let TMP_24 \def (lift TMP_23 O x) in (let TMP_31 \def (\lambda (t:
+T).(let TMP_27 \def (\lambda (u: T).(let TMP_25 \def (S i) in (let TMP_26
+\def (lift TMP_25 O u) in (nf2 c TMP_26)))) in (let TMP_30 \def (\lambda (u:
+T).(let TMP_28 \def (S i) in (let TMP_29 \def (lift TMP_28 O u) in (pc3 c
+TMP_29 t)))) in (ex2 T TMP_27 TMP_30)))) in (let TMP_34 \def (\lambda (u:
+T).(let TMP_32 \def (S i) in (let TMP_33 \def (lift TMP_32 O u) in (nf2 c
+TMP_33)))) in (let TMP_39 \def (\lambda (u: T).(let TMP_35 \def (S i) in (let
+TMP_36 \def (lift TMP_35 O u) in (let TMP_37 \def (S i) in (let TMP_38 \def
+(lift TMP_37 O x) in (pc3 c TMP_36 TMP_38)))))) in (let TMP_40 \def (S i) in
+(let TMP_41 \def (lift TMP_40 O x) in (let TMP_42 \def (pc3_refl c TMP_41) in
+(let TMP_43 \def (ex_intro2 T TMP_34 TMP_39 x H4 TMP_42) in (eq_ind_r T
+TMP_24 TMP_31 TMP_43 u1 H3)))))))))))))))) in (ex_ind T TMP_12 TMP_19 TMP_44
+H2))))))))))))) in (let TMP_145 \def (\lambda (t: T).(\lambda (t0:
+TList).(\lambda (H: ((\forall (u1: T).(\forall (i: nat).((ty3 g c (THeads
+(Flat Appl) t0 (TLRef i)) u1) \to ((nf2 c (TLRef i)) \to ((nf2 c u1) \to (ex2
+T (\lambda (u: T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3 c (THeads
+(Flat Appl) t0 (lift (S i) O u)) u1)))))))))).(\lambda (u1: T).(\lambda (i:
+nat).(\lambda (H0: (ty3 g c (THead (Flat Appl) t (THeads (Flat Appl) t0
+(TLRef i))) u1)).(\lambda (H1: (nf2 c (TLRef i))).(\lambda (_: (nf2 c
+u1)).(let TMP_46 \def (Flat Appl) in (let TMP_47 \def (TLRef i) in (let
+TMP_48 \def (THeads TMP_46 t0 TMP_47) in (let H_x \def (ty3_gen_appl_nf2 g c
+t TMP_48 u1 H0) in (let H3 \def H_x in (let TMP_53 \def (\lambda (u:
+T).(\lambda (t1: T).(let TMP_49 \def (Flat Appl) in (let TMP_50 \def (Bind
+Abst) in (let TMP_51 \def (THead TMP_50 u t1) in (let TMP_52 \def (THead
+TMP_49 t TMP_51) in (pc3 c TMP_52 u1))))))) in (let TMP_59 \def (\lambda (u:
+T).(\lambda (t1: T).(let TMP_54 \def (Flat Appl) in (let TMP_55 \def (TLRef
+i) in (let TMP_56 \def (THeads TMP_54 t0 TMP_55) in (let TMP_57 \def (Bind
+Abst) in (let TMP_58 \def (THead TMP_57 u t1) in (ty3 g c TMP_56
+TMP_58)))))))) in (let TMP_60 \def (\lambda (u: T).(\lambda (_: T).(ty3 g c t
+u))) in (let TMP_63 \def (\lambda (u: T).(\lambda (t1: T).(let TMP_61 \def
+(Bind Abst) in (let TMP_62 \def (THead TMP_61 u t1) in (nf2 c TMP_62))))) in
+(let TMP_66 \def (\lambda (u: T).(let TMP_64 \def (S i) in (let TMP_65 \def
+(lift TMP_64 O u) in (nf2 c TMP_65)))) in (let TMP_73 \def (\lambda (u:
+T).(let TMP_67 \def (Flat Appl) in (let TMP_68 \def (Flat Appl) in (let
+TMP_69 \def (S i) in (let TMP_70 \def (lift TMP_69 O u) in (let TMP_71 \def
+(THeads TMP_68 t0 TMP_70) in (let TMP_72 \def (THead TMP_67 t TMP_71) in (pc3
+c TMP_72 u1)))))))) in (let TMP_74 \def (ex2 T TMP_66 TMP_73) in (let TMP_144
+\def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (pc3 c (THead (Flat
Appl) t (THead (Bind Abst) x0 x1)) u1)).(\lambda (H5: (ty3 g c (THeads (Flat
Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c t
x0)).(\lambda (H7: (nf2 c (THead (Bind Abst) x0 x1))).(let H8 \def
-(nf2_gen_abst c x0 x1 H7) in (land_ind (nf2 c x0) (nf2 (CHead c (Bind Abst)
-x0) x1) (ex2 T (\lambda (u: T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3
-c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))) u1)))
-(\lambda (H9: (nf2 c x0)).(\lambda (H10: (nf2 (CHead c (Bind Abst) x0)
-x1)).(let H_y \def (H (THead (Bind Abst) x0 x1) i H5 H1) in (let H11 \def
-(H_y (nf2_abst_shift c x0 H9 x1 H10)) in (ex2_ind T (\lambda (u: T).(nf2 c
-(lift (S i) O u))) (\lambda (u: T).(pc3 c (THeads (Flat Appl) t0 (lift (S i)
-O u)) (THead (Bind Abst) x0 x1))) (ex2 T (\lambda (u: T).(nf2 c (lift (S i) O
-u))) (\lambda (u: T).(pc3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift
-(S i) O u))) u1))) (\lambda (x: T).(\lambda (H12: (nf2 c (lift (S i) O
-x))).(\lambda (H13: (pc3 c (THeads (Flat Appl) t0 (lift (S i) O x)) (THead
-(Bind Abst) x0 x1))).(ex_intro2 T (\lambda (u: T).(nf2 c (lift (S i) O u)))
-(\lambda (u: T).(pc3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S
-i) O u))) u1)) x H12 (pc3_t (THead (Flat Appl) t (THead (Bind Abst) x0 x1)) c
-(THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O x))) (pc3_thin_dx c
-(THeads (Flat Appl) t0 (lift (S i) O x)) (THead (Bind Abst) x0 x1) H13 t
-Appl) u1 H4))))) H11))))) H8)))))))) H3))))))))))) vs))).
-(* COMMENTS
-Initial nodes: 1213
-END *)
+(nf2_gen_abst c x0 x1 H7) in (let TMP_75 \def (nf2 c x0) in (let TMP_76 \def
+(Bind Abst) in (let TMP_77 \def (CHead c TMP_76 x0) in (let TMP_78 \def (nf2
+TMP_77 x1) in (let TMP_81 \def (\lambda (u: T).(let TMP_79 \def (S i) in (let
+TMP_80 \def (lift TMP_79 O u) in (nf2 c TMP_80)))) in (let TMP_88 \def
+(\lambda (u: T).(let TMP_82 \def (Flat Appl) in (let TMP_83 \def (Flat Appl)
+in (let TMP_84 \def (S i) in (let TMP_85 \def (lift TMP_84 O u) in (let
+TMP_86 \def (THeads TMP_83 t0 TMP_85) in (let TMP_87 \def (THead TMP_82 t
+TMP_86) in (pc3 c TMP_87 u1)))))))) in (let TMP_89 \def (ex2 T TMP_81 TMP_88)
+in (let TMP_143 \def (\lambda (H9: (nf2 c x0)).(\lambda (H10: (nf2 (CHead c
+(Bind Abst) x0) x1)).(let TMP_90 \def (Bind Abst) in (let TMP_91 \def (THead
+TMP_90 x0 x1) in (let H_y \def (H TMP_91 i H5 H1) in (let TMP_92 \def
+(nf2_abst_shift c x0 H9 x1 H10) in (let H11 \def (H_y TMP_92) in (let TMP_95
+\def (\lambda (u: T).(let TMP_93 \def (S i) in (let TMP_94 \def (lift TMP_93
+O u) in (nf2 c TMP_94)))) in (let TMP_102 \def (\lambda (u: T).(let TMP_96
+\def (Flat Appl) in (let TMP_97 \def (S i) in (let TMP_98 \def (lift TMP_97 O
+u) in (let TMP_99 \def (THeads TMP_96 t0 TMP_98) in (let TMP_100 \def (Bind
+Abst) in (let TMP_101 \def (THead TMP_100 x0 x1) in (pc3 c TMP_99
+TMP_101)))))))) in (let TMP_105 \def (\lambda (u: T).(let TMP_103 \def (S i)
+in (let TMP_104 \def (lift TMP_103 O u) in (nf2 c TMP_104)))) in (let TMP_112
+\def (\lambda (u: T).(let TMP_106 \def (Flat Appl) in (let TMP_107 \def (Flat
+Appl) in (let TMP_108 \def (S i) in (let TMP_109 \def (lift TMP_108 O u) in
+(let TMP_110 \def (THeads TMP_107 t0 TMP_109) in (let TMP_111 \def (THead
+TMP_106 t TMP_110) in (pc3 c TMP_111 u1)))))))) in (let TMP_113 \def (ex2 T
+TMP_105 TMP_112) in (let TMP_142 \def (\lambda (x: T).(\lambda (H12: (nf2 c
+(lift (S i) O x))).(\lambda (H13: (pc3 c (THeads (Flat Appl) t0 (lift (S i) O
+x)) (THead (Bind Abst) x0 x1))).(let TMP_116 \def (\lambda (u: T).(let
+TMP_114 \def (S i) in (let TMP_115 \def (lift TMP_114 O u) in (nf2 c
+TMP_115)))) in (let TMP_123 \def (\lambda (u: T).(let TMP_117 \def (Flat
+Appl) in (let TMP_118 \def (Flat Appl) in (let TMP_119 \def (S i) in (let
+TMP_120 \def (lift TMP_119 O u) in (let TMP_121 \def (THeads TMP_118 t0
+TMP_120) in (let TMP_122 \def (THead TMP_117 t TMP_121) in (pc3 c TMP_122
+u1)))))))) in (let TMP_124 \def (Flat Appl) in (let TMP_125 \def (Bind Abst)
+in (let TMP_126 \def (THead TMP_125 x0 x1) in (let TMP_127 \def (THead
+TMP_124 t TMP_126) in (let TMP_128 \def (Flat Appl) in (let TMP_129 \def
+(Flat Appl) in (let TMP_130 \def (S i) in (let TMP_131 \def (lift TMP_130 O
+x) in (let TMP_132 \def (THeads TMP_129 t0 TMP_131) in (let TMP_133 \def
+(THead TMP_128 t TMP_132) in (let TMP_134 \def (Flat Appl) in (let TMP_135
+\def (S i) in (let TMP_136 \def (lift TMP_135 O x) in (let TMP_137 \def
+(THeads TMP_134 t0 TMP_136) in (let TMP_138 \def (Bind Abst) in (let TMP_139
+\def (THead TMP_138 x0 x1) in (let TMP_140 \def (pc3_thin_dx c TMP_137
+TMP_139 H13 t Appl) in (let TMP_141 \def (pc3_t TMP_127 c TMP_133 TMP_140 u1
+H4) in (ex_intro2 T TMP_116 TMP_123 x H12 TMP_141)))))))))))))))))))))))) in
+(ex2_ind T TMP_95 TMP_102 TMP_113 TMP_142 H11)))))))))))))) in (land_ind
+TMP_75 TMP_78 TMP_89 TMP_143 H8)))))))))))))))) in (ex4_2_ind T T TMP_53
+TMP_59 TMP_60 TMP_63 TMP_74 TMP_144 H3)))))))))))))))))))))) in (TList_ind
+TMP_9 TMP_45 TMP_145 vs)))))).
theorem ty3_inv_lref_lref_nf2:
\forall (g: G).(\forall (c: C).(\forall (i: nat).(\forall (j: nat).((ty3 g c
\def
\lambda (g: G).(\lambda (c: C).(\lambda (i: nat).(\lambda (j: nat).(\lambda
(H: (ty3 g c (TLRef i) (TLRef j))).(\lambda (H0: (nf2 c (TLRef i))).(\lambda
-(H1: (nf2 c (TLRef j))).(let H_x \def (ty3_inv_lref_nf2 g c (TLRef j) i H H0
-H1) in (let H2 \def H_x in (ex_ind T (\lambda (u0: T).(eq T (TLRef j) (lift
-(S i) O u0))) (lt i j) (\lambda (x: T).(\lambda (H3: (eq T (TLRef j) (lift (S
-i) O x))).(let H_x0 \def (lift_gen_lref x O (S i) j H3) in (let H4 \def H_x0
-in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (S i) j) (eq T x
-(TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x
-(TLRef j)))).(land_ind (lt j O) (eq T x (TLRef j)) (lt i j) (\lambda (H6: (lt
-j O)).(\lambda (_: (eq T x (TLRef j))).(lt_x_O j H6 (lt i j)))) H5)) (\lambda
-(H5: (land (le (S i) j) (eq T x (TLRef (minus j (S i)))))).(land_ind (le (S
-i) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6: (le (S i)
-j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) H5)) H4)))))
-H2))))))))).
-(* COMMENTS
-Initial nodes: 337
-END *)
+(H1: (nf2 c (TLRef j))).(let TMP_1 \def (TLRef j) in (let H_x \def
+(ty3_inv_lref_nf2 g c TMP_1 i H H0 H1) in (let H2 \def H_x in (let TMP_5 \def
+(\lambda (u0: T).(let TMP_2 \def (TLRef j) in (let TMP_3 \def (S i) in (let
+TMP_4 \def (lift TMP_3 O u0) in (eq T TMP_2 TMP_4))))) in (let TMP_6 \def (lt
+i j) in (let TMP_36 \def (\lambda (x: T).(\lambda (H3: (eq T (TLRef j) (lift
+(S i) O x))).(let TMP_7 \def (S i) in (let H_x0 \def (lift_gen_lref x O TMP_7
+j H3) in (let H4 \def H_x0 in (let TMP_8 \def (lt j O) in (let TMP_9 \def
+(TLRef j) in (let TMP_10 \def (eq T x TMP_9) in (let TMP_11 \def (land TMP_8
+TMP_10) in (let TMP_12 \def (S i) in (let TMP_13 \def (le TMP_12 j) in (let
+TMP_14 \def (S i) in (let TMP_15 \def (minus j TMP_14) in (let TMP_16 \def
+(TLRef TMP_15) in (let TMP_17 \def (eq T x TMP_16) in (let TMP_18 \def (land
+TMP_13 TMP_17) in (let TMP_19 \def (lt i j) in (let TMP_26 \def (\lambda (H5:
+(land (lt j O) (eq T x (TLRef j)))).(let TMP_20 \def (lt j O) in (let TMP_21
+\def (TLRef j) in (let TMP_22 \def (eq T x TMP_21) in (let TMP_23 \def (lt i
+j) in (let TMP_25 \def (\lambda (H6: (lt j O)).(\lambda (_: (eq T x (TLRef
+j))).(let TMP_24 \def (lt i j) in (lt_x_O j H6 TMP_24)))) in (land_ind TMP_20
+TMP_22 TMP_23 TMP_25 H5))))))) in (let TMP_35 \def (\lambda (H5: (land (le (S
+i) j) (eq T x (TLRef (minus j (S i)))))).(let TMP_27 \def (S i) in (let
+TMP_28 \def (le TMP_27 j) in (let TMP_29 \def (S i) in (let TMP_30 \def
+(minus j TMP_29) in (let TMP_31 \def (TLRef TMP_30) in (let TMP_32 \def (eq T
+x TMP_31) in (let TMP_33 \def (lt i j) in (let TMP_34 \def (\lambda (H6: (le
+(S i) j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6)) in (land_ind
+TMP_28 TMP_32 TMP_33 TMP_34 H5)))))))))) in (or_ind TMP_11 TMP_18 TMP_19
+TMP_26 TMP_35 H4)))))))))))))))))))) in (ex_ind T TMP_5 TMP_6 TMP_36
+H2))))))))))))).