-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
-False])) I (THead (Bind Abst) v t) H) in (False_ind P H0)))))))) (\lambda (n:
-nat).(\lambda (v: T).(or_intror (ex T (\lambda (t: T).(eq T (TLRef n) (THead
-(Bind Abst) v t)))) (\forall (t: T).((eq T (TLRef n) (THead (Bind Abst) v t))
-\to (\forall (P: Prop).P))) (\lambda (t: T).(\lambda (H: (eq T (TLRef n)
-(THead (Bind Abst) v t))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TLRef n)
-(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
-False])) I (THead (Bind Abst) v t) H) in (False_ind P H0)))))))) (\lambda (k:
-K).(\lambda (t: T).(\lambda (_: ((\forall (v: T).(or (ex T (\lambda (t0:
-T).(eq T t (THead (Bind Abst) v t0)))) (\forall (t0: T).((eq T t (THead (Bind
-Abst) v t0)) \to (\forall (P: Prop).P))))))).(\lambda (t0: T).(\lambda (_:
-((\forall (v: T).(or (ex T (\lambda (t1: T).(eq T t0 (THead (Bind Abst) v
-t1)))) (\forall (t1: T).((eq T t0 (THead (Bind Abst) v t1)) \to (\forall (P:
-Prop).P))))))).(\lambda (v: T).(let H_x \def (terms_props__kind_dec k (Bind
-Abst)) in (let H1 \def H_x in (or_ind (eq K k (Bind Abst)) ((eq K k (Bind
-Abst)) \to (\forall (P: Prop).P)) (or (ex T (\lambda (t1: T).(eq T (THead k t
-t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k t t0) (THead
-(Bind Abst) v t1)) \to (\forall (P: Prop).P)))) (\lambda (H2: (eq K k (Bind
-Abst))).(eq_ind_r K (Bind Abst) (\lambda (k0: K).(or (ex T (\lambda (t1:
-T).(eq T (THead k0 t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T
-(THead k0 t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))))) (let
-H_x0 \def (term_dec t v) in (let H3 \def H_x0 in (or_ind (eq T t v) ((eq T t
-v) \to (\forall (P: Prop).P)) (or (ex T (\lambda (t1: T).(eq T (THead (Bind
-Abst) t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead (Bind
-Abst) t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P)))) (\lambda
-(H4: (eq T t v)).(eq_ind T t (\lambda (t1: T).(or (ex T (\lambda (t2: T).(eq
-T (THead (Bind Abst) t t0) (THead (Bind Abst) t1 t2)))) (\forall (t2: T).((eq
-T (THead (Bind Abst) t t0) (THead (Bind Abst) t1 t2)) \to (\forall (P:
-Prop).P))))) (or_introl (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0)
-(THead (Bind Abst) t t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0)
-(THead (Bind Abst) t t1)) \to (\forall (P: Prop).P))) (ex_intro T (\lambda
-(t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1))) t0
-(refl_equal T (THead (Bind Abst) t t0)))) v H4)) (\lambda (H4: (((eq T t v)
-\to (\forall (P: Prop).P)))).(or_intror (ex T (\lambda (t1: T).(eq T (THead
-(Bind Abst) t t0) (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead
-(Bind Abst) t t0) (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P)))
-(\lambda (t1: T).(\lambda (H5: (eq T (THead (Bind Abst) t t0) (THead (Bind
-Abst) v t1))).(\lambda (P: Prop).(let H6 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t |
-(TLRef _) \Rightarrow t | (THead _ t2 _) \Rightarrow t2])) (THead (Bind Abst)
-t t0) (THead (Bind Abst) v t1) H5) in ((let H7 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 |
-(TLRef _) \Rightarrow t0 | (THead _ _ t2) \Rightarrow t2])) (THead (Bind
-Abst) t t0) (THead (Bind Abst) v t1) H5) in (\lambda (H8: (eq T t v)).(H4 H8
-P))) H6))))))) H3))) k H2)) (\lambda (H2: (((eq K k (Bind Abst)) \to (\forall
-(P: Prop).P)))).(or_intror (ex T (\lambda (t1: T).(eq T (THead k t t0) (THead
-(Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k t t0) (THead (Bind
-Abst) v t1)) \to (\forall (P: Prop).P))) (\lambda (t1: T).(\lambda (H3: (eq T
-(THead k t t0) (THead (Bind Abst) v t1))).(\lambda (P: Prop).(let H4 \def
-(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with
-[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
-\Rightarrow k0])) (THead k t t0) (THead (Bind Abst) v t1) H3) in ((let H5
-\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
+(ee: T).(match ee with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow
+False | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) v t) H) in
+(False_ind P H0)))))))) (\lambda (n: nat).(\lambda (v: T).(or_intror (ex T
+(\lambda (t: T).(eq T (TLRef n) (THead (Bind Abst) v t)))) (\forall (t:
+T).((eq T (TLRef n) (THead (Bind Abst) v t)) \to (\forall (P: Prop).P)))
+(\lambda (t: T).(\lambda (H: (eq T (TLRef n) (THead (Bind Abst) v
+t))).(\lambda (P: Prop).(let H0 \def (eq_ind T (TLRef n) (\lambda (ee:
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
+(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) v t) H) in (False_ind
+P H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (_: ((\forall (v:
+T).(or (ex T (\lambda (t0: T).(eq T t (THead (Bind Abst) v t0)))) (\forall
+(t0: T).((eq T t (THead (Bind Abst) v t0)) \to (\forall (P:
+Prop).P))))))).(\lambda (t0: T).(\lambda (_: ((\forall (v: T).(or (ex T
+(\lambda (t1: T).(eq T t0 (THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T
+t0 (THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))))))).(\lambda (v:
+T).(let H_x \def (terms_props__kind_dec k (Bind Abst)) in (let H1 \def H_x in
+(or_ind (eq K k (Bind Abst)) ((eq K k (Bind Abst)) \to (\forall (P: Prop).P))
+(or (ex T (\lambda (t1: T).(eq T (THead k t t0) (THead (Bind Abst) v t1))))
+(\forall (t1: T).((eq T (THead k t t0) (THead (Bind Abst) v t1)) \to (\forall
+(P: Prop).P)))) (\lambda (H2: (eq K k (Bind Abst))).(eq_ind_r K (Bind Abst)
+(\lambda (k0: K).(or (ex T (\lambda (t1: T).(eq T (THead k0 t t0) (THead
+(Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead k0 t t0) (THead (Bind
+Abst) v t1)) \to (\forall (P: Prop).P))))) (let H_x0 \def (term_dec t v) in
+(let H3 \def H_x0 in (or_ind (eq T t v) ((eq T t v) \to (\forall (P:
+Prop).P)) (or (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead
+(Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0) (THead
+(Bind Abst) v t1)) \to (\forall (P: Prop).P)))) (\lambda (H4: (eq T t
+v)).(eq_ind T t (\lambda (t1: T).(or (ex T (\lambda (t2: T).(eq T (THead
+(Bind Abst) t t0) (THead (Bind Abst) t1 t2)))) (\forall (t2: T).((eq T (THead
+(Bind Abst) t t0) (THead (Bind Abst) t1 t2)) \to (\forall (P: Prop).P)))))
+(or_introl (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0) (THead (Bind
+Abst) t t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0) (THead (Bind
+Abst) t t1)) \to (\forall (P: Prop).P))) (ex_intro T (\lambda (t1: T).(eq T
+(THead (Bind Abst) t t0) (THead (Bind Abst) t t1))) t0 (refl_equal T (THead
+(Bind Abst) t t0)))) v H4)) (\lambda (H4: (((eq T t v) \to (\forall (P:
+Prop).P)))).(or_intror (ex T (\lambda (t1: T).(eq T (THead (Bind Abst) t t0)
+(THead (Bind Abst) v t1)))) (\forall (t1: T).((eq T (THead (Bind Abst) t t0)
+(THead (Bind Abst) v t1)) \to (\forall (P: Prop).P))) (\lambda (t1:
+T).(\lambda (H5: (eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v
+t1))).(\lambda (P: Prop).(let H6 \def (f_equal T T (\lambda (e: T).(match e