-((\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))))).(match k in K return
-(\lambda (k0: K).(or (\forall (t2: T).((pr2 (CTail k0 t c0) t1 t2) \to (eq T
-t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
-(\lambda (t2: T).(pr2 (CTail k0 t c0) t1 t2))))) with [(Bind b) \Rightarrow
-(match b in B return (\lambda (b0: B).(or (\forall (t2: T).((pr2 (CTail (Bind
-b0) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind b0) t c0) t1
-t2))))) with [Abbr \Rightarrow (let H_x0 \def (dnf_dec t t1 (clen c0)) in
-(let H2 \def H_x0 in (ex_ind T (\lambda (v: T).(or (subst0 (clen c0) t t1
-(lift (S O) (clen c0) v)) (eq T t1 (lift (S O) (clen c0) v)))) (or (\forall
-(t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T
-(\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
-T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda (x: T).(\lambda (H3: (or
-(subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq T t1 (lift (S O) (clen
-c0) x)))).(or_ind (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq T t1
-(lift (S O) (clen c0) x)) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0)
-t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
-(P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2))))
-(\lambda (H4: (subst0 (clen c0) t t1 (lift (S O) (clen c0) x))).(let H_x1
-\def (getl_ctail_clen Abbr t c0) in (let H5 \def H_x1 in (ex_ind nat (\lambda
-(n: nat).(getl (clen c0) (CTail (Bind Abbr) t c0) (CHead (CSort n) (Bind
-Abbr) t))) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2) \to (eq
-T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
-(\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda (x0:
-nat).(\lambda (H6: (getl (clen c0) (CTail (Bind Abbr) t c0) (CHead (CSort x0)
-(Bind Abbr) t))).(or_intror (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0)
-t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
-(P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))
-(ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
-(\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)) (lift (S O) (clen c0)
-x) (\lambda (H7: (eq T t1 (lift (S O) (clen c0) x))).(\lambda (P: Prop).(let
-H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0 (clen c0) t t0 (lift (S O)
-(clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in (subst0_gen_lift_false x t
-(lift (S O) (clen c0) x) (S O) (clen c0) (clen c0) (le_n (clen c0)) (eq_ind_r
-nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt (clen c0) n)) (le_n (plus (S
-O) (clen c0))) (plus (clen c0) (S O)) (plus_comm (clen c0) (S O))) H8 P))))
-(pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t (clen c0) H6 t1 t1 (pr0_refl
-t1) (lift (S O) (clen c0) x) H4))))) H5)))) (\lambda (H4: (eq T t1 (lift (S
-O) (clen c0) x))).(let H5 \def (eq_ind T t1 (\lambda (t0: T).(\forall (t2:
-T).((pr2 c0 t0 t2) \to (eq T t0 t2)))) H1 (lift (S O) (clen c0) x) H4) in
-(eq_ind_r T (lift (S O) (clen c0) x) (\lambda (t0: T).(or (\forall (t2:
-T).((pr2 (CTail (Bind Abbr) t c0) t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda
-(t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2
-(CTail (Bind Abbr) t c0) t0 t2))))) (or_introl (\forall (t2: T).((pr2 (CTail
-(Bind Abbr) t c0) (lift (S O) (clen c0) x) t2) \to (eq T (lift (S O) (clen
-c0) x) t2))) (ex2 T (\lambda (t2: T).((eq T (lift (S O) (clen c0) x) t2) \to
-(\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) (lift
-(S O) (clen c0) x) t2))) (\lambda (t2: T).(\lambda (H6: (pr2 (CTail (Bind
-Abbr) t c0) (lift (S O) (clen c0) x) t2)).(let H_x1 \def (pr2_gen_ctail (Bind
-Abbr) c0 t (lift (S O) (clen c0) x) t2 H6) in (let H7 \def H_x1 in (or_ind
-(pr2 c0 (lift (S O) (clen c0) x) t2) (ex3 T (\lambda (_: T).(eq K (Bind Abbr)
+((\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))))).(K_ind (\lambda (k0:
+K).(or (\forall (t2: T).((pr2 (CTail k0 t c0) t1 t2) \to (eq T t1 t2))) (ex2
+T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
+T).(pr2 (CTail k0 t c0) t1 t2))))) (\lambda (b: B).(B_ind (\lambda (b0:
+B).(or (\forall (t2: T).((pr2 (CTail (Bind b0) t c0) t1 t2) \to (eq T t1
+t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr2 (CTail (Bind b0) t c0) t1 t2))))) (let H_x0 \def
+(dnf_dec t t1 (clen c0)) in (let H2 \def H_x0 in (ex_ind T (\lambda (v:
+T).(or (subst0 (clen c0) t t1 (lift (S O) (clen c0) v)) (eq T t1 (lift (S O)
+(clen c0) v)))) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2)
+\to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P:
+Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda
+(x: T).(\lambda (H3: (or (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq
+T t1 (lift (S O) (clen c0) x)))).(or_ind (subst0 (clen c0) t t1 (lift (S O)
+(clen c0) x)) (eq T t1 (lift (S O) (clen c0) x)) (or (\forall (t2: T).((pr2
+(CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
+T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
+(Bind Abbr) t c0) t1 t2)))) (\lambda (H4: (subst0 (clen c0) t t1 (lift (S O)
+(clen c0) x))).(let H_x1 \def (getl_ctail_clen Abbr t c0) in (let H5 \def
+H_x1 in (ex_ind nat (\lambda (n: nat).(getl (clen c0) (CTail (Bind Abbr) t
+c0) (CHead (CSort n) (Bind Abbr) t))) (or (\forall (t2: T).((pr2 (CTail (Bind
+Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2)
+\to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1
+t2)))) (\lambda (x0: nat).(\lambda (H6: (getl (clen c0) (CTail (Bind Abbr) t
+c0) (CHead (CSort x0) (Bind Abbr) t))).(or_intror (\forall (t2: T).((pr2
+(CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
+T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
+(Bind Abbr) t c0) t1 t2))) (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to
+(\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1
+t2)) (lift (S O) (clen c0) x) (\lambda (H7: (eq T t1 (lift (S O) (clen c0)
+x))).(\lambda (P: Prop).(let H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0
+(clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in
+(subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0)
+(le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt
+(clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_comm
+(clen c0) (S O))) H8 P)))) (pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t
+(clen c0) H6 t1 t1 (pr0_refl t1) (lift (S O) (clen c0) x) H4))))) H5))))
+(\lambda (H4: (eq T t1 (lift (S O) (clen c0) x))).(let H5 \def (eq_ind T t1
+(\lambda (t0: T).(\forall (t2: T).((pr2 c0 t0 t2) \to (eq T t0 t2)))) H1
+(lift (S O) (clen c0) x) H4) in (eq_ind_r T (lift (S O) (clen c0) x) (\lambda
+(t0: T).(or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t0 t2) \to (eq T
+t0 t2))) (ex2 T (\lambda (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P)))
+(\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t0 t2))))) (or_introl (\forall
+(t2: T).((pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2) \to (eq T
+(lift (S O) (clen c0) x) t2))) (ex2 T (\lambda (t2: T).((eq T (lift (S O)
+(clen c0) x) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail
+(Bind Abbr) t c0) (lift (S O) (clen c0) x) t2))) (\lambda (t2: T).(\lambda
+(H6: (pr2 (CTail (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2)).(let H_x1
+\def (pr2_gen_ctail (Bind Abbr) c0 t (lift (S O) (clen c0) x) t2 H6) in (let
+H7 \def H_x1 in (or_ind (pr2 c0 (lift (S O) (clen c0) x) t2) (ex3 T (\lambda
+(_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda (t0: T).(pr0 (lift (S O)
+(clen c0) x) t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2))) (eq T (lift
+(S O) (clen c0) x) t2) (\lambda (H8: (pr2 c0 (lift (S O) (clen c0) x)
+t2)).(H5 t2 H8)) (\lambda (H8: (ex3 T (\lambda (_: T).(eq K (Bind Abbr) (Bind
+Abbr))) (\lambda (t0: T).(pr0 (lift (S O) (clen c0) x) t0)) (\lambda (t0:
+T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Bind Abbr)