-in (let TMP_7 \def (\lambda (v: T).(let TMP_1 \def (S O) in (let TMP_2 \def
-(lift TMP_1 O v) in (let TMP_3 \def (subst0 O u t TMP_2) in (let TMP_4 \def
-(S O) in (let TMP_5 \def (lift TMP_4 O v) in (let TMP_6 \def (eq T t TMP_5)
-in (or TMP_3 TMP_6)))))))) in (let TMP_60 \def (\lambda (x: T).(\lambda (H1:
-(or (subst0 O u t (lift (S O) O x)) (eq T t (lift (S O) O x)))).(let TMP_8
-\def (S O) in (let TMP_9 \def (lift TMP_8 O x) in (let TMP_10 \def (subst0 O
-u t TMP_9) in (let TMP_11 \def (S O) in (let TMP_12 \def (lift TMP_11 O x) in
-(let TMP_13 \def (eq T t TMP_12) in (let TMP_45 \def (\lambda (H2: (subst0 O
-u t (lift (S O) O x))).(let TMP_14 \def (\lambda (e: T).(match e with [(TSort
-_) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
-in (let TMP_15 \def (Bind Abbr) in (let TMP_16 \def (THead TMP_15 u t) in
-(let TMP_17 \def (Bind Abbr) in (let TMP_18 \def (S O) in (let TMP_19 \def
-(lift TMP_18 O x) in (let TMP_20 \def (THead TMP_17 u TMP_19) in (let TMP_21
-\def (Bind Abbr) in (let TMP_22 \def (S O) in (let TMP_23 \def (lift TMP_22 O
-x) in (let TMP_24 \def (THead TMP_21 u TMP_23) in (let TMP_25 \def (Bind
-Abbr) in (let TMP_26 \def (THead TMP_25 u t) in (let TMP_27 \def (Bind Abbr)
-in (let TMP_28 \def (S O) in (let TMP_29 \def (lift TMP_28 O x) in (let
-TMP_30 \def (THead TMP_27 u TMP_29) in (let TMP_31 \def (pr0_refl u) in (let
-TMP_32 \def (pr0_refl t) in (let TMP_33 \def (S O) in (let TMP_34 \def (lift
-TMP_33 O x) in (let TMP_35 \def (pr0_delta u u TMP_31 t t TMP_32 TMP_34 H2)
-in (let TMP_36 \def (pr2_free c TMP_26 TMP_30 TMP_35) in (let TMP_37 \def (H
-TMP_24 TMP_36) in (let H3 \def (f_equal T T TMP_14 TMP_16 TMP_20 TMP_37) in
-(let TMP_40 \def (\lambda (t0: T).(let TMP_38 \def (S O) in (let TMP_39 \def
-(lift TMP_38 O x) in (subst0 O u t0 TMP_39)))) in (let TMP_41 \def (S O) in
-(let TMP_42 \def (lift TMP_41 O x) in (let H4 \def (eq_ind T t TMP_40 H2
-TMP_42 H3) in (let TMP_43 \def (S O) in (let TMP_44 \def (lift TMP_43 O x) in
-(subst0_refl u TMP_44 O H4 P))))))))))))))))))))))))))))))))) in (let TMP_59
-\def (\lambda (H2: (eq T t (lift (S O) O x))).(let TMP_48 \def (\lambda (t0:
-T).(\forall (t2: T).((pr2 c (THead (Bind Abbr) u t0) t2) \to (let TMP_46 \def
-(Bind Abbr) in (let TMP_47 \def (THead TMP_46 u t0) in (eq T TMP_47 t2))))))
-in (let TMP_49 \def (S O) in (let TMP_50 \def (lift TMP_49 O x) in (let H3
-\def (eq_ind T t TMP_48 H TMP_50 H2) in (let TMP_51 \def (Bind Abbr) in (let
-TMP_52 \def (S O) in (let TMP_53 \def (lift TMP_52 O x) in (let TMP_54 \def
-(THead TMP_51 u TMP_53) in (let TMP_55 \def (pr0_refl x) in (let TMP_56 \def
-(pr0_zeta Abbr not_abbr_abst x x TMP_55 u) in (let TMP_57 \def (pr2_free c
-TMP_54 x TMP_56) in (let TMP_58 \def (H3 x TMP_57) in (nf2_gen__nf2_gen_aux
-Abbr x u O TMP_58 P)))))))))))))) in (or_ind TMP_10 TMP_13 P TMP_45 TMP_59
-H1))))))))))) in (ex_ind T TMP_7 P TMP_60 H0))))))))).
+in (ex_ind T (\lambda (v: T).(or (subst0 O u t (lift (S O) O v)) (eq T t
+(lift (S O) O v)))) P (\lambda (x: T).(\lambda (H1: (or (subst0 O u t (lift
+(S O) O x)) (eq T t (lift (S O) O x)))).(or_ind (subst0 O u t (lift (S O) O
+x)) (eq T t (lift (S O) O x)) P (\lambda (H2: (subst0 O u t (lift (S O) O
+x))).(let H3 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
+\Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
+(THead (Bind Abbr) u t) (THead (Bind Abbr) u (lift (S O) O x)) (H (THead
+(Bind Abbr) u (lift (S O) O x)) (pr2_free c (THead (Bind Abbr) u t) (THead
+(Bind Abbr) u (lift (S O) O x)) (pr0_delta u u (pr0_refl u) t t (pr0_refl t)
+(lift (S O) O x) H2)))) in (let H4 \def (eq_ind T t (\lambda (t0: T).(subst0
+O u t0 (lift (S O) O x))) H2 (lift (S O) O x) H3) in (subst0_refl u (lift (S
+O) O x) O H4 P)))) (\lambda (H2: (eq T t (lift (S O) O x))).(let H3 \def
+(eq_ind T t (\lambda (t0: T).(\forall (t2: T).((pr2 c (THead (Bind Abbr) u
+t0) t2) \to (eq T (THead (Bind Abbr) u t0) t2)))) H (lift (S O) O x) H2) in
+(nf2_gen__nf2_gen_aux Abbr x u O (H3 x (pr2_free c (THead (Bind Abbr) u (lift
+(S O) O x)) x (pr0_zeta Abbr not_abbr_abst x x (pr0_refl x) u))) P))) H1)))
+H0))))))).