-x0 x4 H22 Appl) x1 x4 (refl_equal T (THead (Flat Appl) (lift (S O) O x1)
-x4)))) H28))) x3 H25)))) (\lambda (H25: (((eq T t1 x3) \to (\forall (P:
-Prop).P)))).(H2 x3 H25 H21 x4 x1 (sn3_cpr3_trans c t1 x3 H21 (Bind b) (THead
-(Flat Appl) (lift (S O) O x1) x4) (let H_x1 \def (term_dec x0 x4) in (let H26
-\def H_x1 in (or_ind (eq T x0 x4) ((eq T x0 x4) \to (\forall (P: Prop).P))
-(sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)) (\lambda
-(H27: (eq T x0 x4)).(let H28 \def (eq_ind_r T x4 (\lambda (t0: T).(pr3 (CHead
-c (Bind b) t1) x0 t0)) H22 x0 H27) in (eq_ind T x0 (\lambda (t0: T).(sn3
-(CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) t0))) (let H_x2
-\def (term_dec x x1) in (let H29 \def H_x2 in (or_ind (eq T x x1) ((eq T x
-x1) \to (\forall (P: Prop).P)) (sn3 (CHead c (Bind b) t1) (THead (Flat Appl)
-(lift (S O) O x1) x0)) (\lambda (H30: (eq T x x1)).(let H31 \def (eq_ind_r T
-x1 (\lambda (t0: T).(pr2 c x t0)) H15 x H30) in (eq_ind T x (\lambda (t0:
-T).(sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O t0) x0)))
-(sn3_sing (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) H9)
-x1 H30))) (\lambda (H30: (((eq T x x1) \to (\forall (P: Prop).P)))).(H9
-(THead (Flat Appl) (lift (S O) O x1) x0) (\lambda (H31: (eq T (THead (Flat
-Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
-x0))).(\lambda (P: Prop).(let H32 \def (f_equal T T (\lambda (e: T).(match e
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map
-(f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match t0 with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t4)
-\Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d) t4))]) in
-lref_map) (\lambda (x5: nat).(plus x5 (S O))) O x) | (TLRef _) \Rightarrow
-((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match
-t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) |
-(THead k u0 t4) \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d)
-t4))]) in lref_map) (\lambda (x5: nat).(plus x5 (S O))) O x) | (THead _ t0 _)
-\Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl)
-(lift (S O) O x1) x0) H31) in (let H33 \def (eq_ind_r T x1 (\lambda (t0:
-T).((eq T x t0) \to (\forall (P0: Prop).P0))) H30 x (lift_inj x x1 (S O) O
-H32)) in (let H34 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x
-(lift_inj x x1 (S O) O H32)) in (H33 (refl_equal T x) P)))))) (pr3_flat
-(CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1) (pr3_lift (CHead c
-(Bind b) t1) c (S O) O (drop_drop (Bind b) O c c (drop_refl c) t1) x x1
-(pr3_pr2 c x x1 H15)) x0 x0 (pr3_refl (CHead c (Bind b) t1) x0) Appl)))
-H29))) x4 H27))) (\lambda (H27: (((eq T x0 x4) \to (\forall (P:
-Prop).P)))).(H9 (THead (Flat Appl) (lift (S O) O x1) x4) (\lambda (H28: (eq T
-(THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
-x4))).(\lambda (P: Prop).(let H29 \def (f_equal T T (\lambda (e: T).(match e
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map
-(f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match t0 with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t4)
-\Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d) t4))]) in
-lref_map) (\lambda (x5: nat).(plus x5 (S O))) O x) | (TLRef _) \Rightarrow
-((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match
-t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) |
-(THead k u0 t4) \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d)
-t4))]) in lref_map) (\lambda (x5: nat).(plus x5 (S O))) O x) | (THead _ t0 _)
-\Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl)
-(lift (S O) O x1) x4) H28) in ((let H30 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x0 |
-(TLRef _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Flat
-Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1) x4) H28) in
-(\lambda (H31: (eq T (lift (S O) O x) (lift (S O) O x1))).(let H32 \def
-(eq_ind_r T x4 (\lambda (t0: T).((eq T x0 t0) \to (\forall (P0: Prop).P0)))
-H27 x0 H30) in (let H33 \def (eq_ind_r T x4 (\lambda (t0: T).(pr3 (CHead c
-(Bind b) t1) x0 t0)) H22 x0 H30) in (let H34 \def (eq_ind_r T x1 (\lambda
-(t0: T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O) O H31)) in (H32 (refl_equal
-T x0) P)))))) H29)))) (pr3_flat (CHead c (Bind b) t1) (lift (S O) O x) (lift
-(S O) O x1) (pr3_lift (CHead c (Bind b) t1) c (S O) O (drop_drop (Bind b) O c
-c (drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15)) x0 x4 H22 Appl))) H26))))))
-H24))) x2 H20))))))) H19)) (\lambda (H19: (pr3 (CHead c (Bind b) t1) x0 (lift
-(S O) O x2))).(sn3_gen_lift (CHead c (Bind b) t1) (THead (Flat Appl) x1 x2)
-(S O) O (eq_ind_r T (THead (Flat Appl) (lift (S O) O x1) (lift (S O) (s (Flat
-Appl) O) x2)) (\lambda (t0: T).(sn3 (CHead c (Bind b) t1) t0)) (sn3_pr3_trans
-(CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0) (let H_x0 \def
-(term_dec x x1) in (let H20 \def H_x0 in (or_ind (eq T x x1) ((eq T x x1) \to
-(\forall (P: Prop).P)) (sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S
-O) O x1) x0)) (\lambda (H21: (eq T x x1)).(let H22 \def (eq_ind_r T x1
-(\lambda (t0: T).(pr2 c x t0)) H15 x H21) in (eq_ind T x (\lambda (t0:
-T).(sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O t0) x0)))
-(sn3_sing (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) H9)
-x1 H21))) (\lambda (H21: (((eq T x x1) \to (\forall (P: Prop).P)))).(H9
-(THead (Flat Appl) (lift (S O) O x1) x0) (\lambda (H22: (eq T (THead (Flat
-Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
-x0))).(\lambda (P: Prop).(let H23 \def (f_equal T T (\lambda (e: T).(match e
-in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow ((let rec lref_map
-(f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match t0 with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u0 t4)
-\Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d) t4))]) in
-lref_map) (\lambda (x3: nat).(plus x3 (S O))) O x) | (TLRef _) \Rightarrow
-((let rec lref_map (f: ((nat \to nat))) (d: nat) (t0: T) on t0: T \def (match
-t0 with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef
-(match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) |
-(THead k u0 t4) \Rightarrow (THead k (lref_map f d u0) (lref_map f (s k d)
-t4))]) in lref_map) (\lambda (x3: nat).(plus x3 (S O))) O x) | (THead _ t0 _)
-\Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl)
-(lift (S O) O x1) x0) H22) in (let H24 \def (eq_ind_r T x1 (\lambda (t0:
-T).((eq T x t0) \to (\forall (P0: Prop).P0))) H21 x (lift_inj x x1 (S O) O
-H23)) in (let H25 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x
-(lift_inj x x1 (S O) O H23)) in (H24 (refl_equal T x) P)))))) (pr3_flat
-(CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1) (pr3_lift (CHead c
-(Bind b) t1) c (S O) O (drop_drop (Bind b) O c c (drop_refl c) t1) x x1
-(pr3_pr2 c x x1 H15)) x0 x0 (pr3_refl (CHead c (Bind b) t1) x0) Appl)))
-H20))) (THead (Flat Appl) (lift (S O) O x1) (lift (S O) O x2)) (pr3_thin_dx
-(CHead c (Bind b) t1) x0 (lift (S O) O x2) H19 (lift (S O) O x1) Appl)) (lift
-(S O) O (THead (Flat Appl) x1 x2)) (lift_head (Flat Appl) x1 x2 (S O) O)) c
-(drop_drop (Bind b) O c c (drop_refl c) t1))) H18))) t3 H14))))))) H13))
-(\lambda (H13: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
-T).(\lambda (_: T).(eq T (THead (Bind b) t1 x0) (THead (Bind Abst) y1
-z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4:
-T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
+x0 x4 H22 Appl))) H26)))))) H24))) x2 H20))))))) H19)) (\lambda (H19: (pr3
+(CHead c (Bind b) t1) x0 (lift (S O) O x2))).(sn3_gen_lift (CHead c (Bind b)
+t1) (THead (Flat Appl) x1 x2) (S O) O (eq_ind_r T (THead (Flat Appl) (lift (S
+O) O x1) (lift (S O) (s (Flat Appl) O) x2)) (\lambda (t0: T).(sn3 (CHead c
+(Bind b) t1) t0)) (sn3_pr3_trans (CHead c (Bind b) t1) (THead (Flat Appl)
+(lift (S O) O x1) x0) (let H_x0 \def (term_dec x x1) in (let H20 \def H_x0 in
+(or_ind (eq T x x1) ((eq T x x1) \to (\forall (P: Prop).P)) (sn3 (CHead c
+(Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)) (\lambda (H21: (eq T x
+x1)).(let H22 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x H21)
+in (eq_ind T x (\lambda (t0: T).(sn3 (CHead c (Bind b) t1) (THead (Flat Appl)
+(lift (S O) O t0) x0))) (sn3_sing (CHead c (Bind b) t1) (THead (Flat Appl)
+(lift (S O) O x) x0) H9) x1 H21))) (\lambda (H21: (((eq T x x1) \to (\forall
+(P: Prop).P)))).(H9 (THead (Flat Appl) (lift (S O) O x1) x0) (\lambda (H22:
+(eq T (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O)
+O x1) x0))).(\lambda (P: Prop).(let H23 \def (f_equal T T (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow (lref_map (\lambda (x3: nat).(plus x3
+(S O))) O x) | (TLRef _) \Rightarrow (lref_map (\lambda (x3: nat).(plus x3 (S
+O))) O x) | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O
+x) x0) (THead (Flat Appl) (lift (S O) O x1) x0) H22) in (let H24 \def
+(eq_ind_r T x1 (\lambda (t0: T).((eq T x t0) \to (\forall (P0: Prop).P0)))
+H21 x (lift_inj x x1 (S O) O H23)) in (let H25 \def (eq_ind_r T x1 (\lambda
+(t0: T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O) O H23)) in (H24 (refl_equal
+T x) P)))))) (pr3_flat (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O
+x1) (pr3_lift (CHead c (Bind b) t1) c (S O) O (drop_drop (Bind b) O c c
+(drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15)) x0 x0 (pr3_refl (CHead c (Bind
+b) t1) x0) Appl))) H20))) (THead (Flat Appl) (lift (S O) O x1) (lift (S O) O
+x2)) (pr3_thin_dx (CHead c (Bind b) t1) x0 (lift (S O) O x2) H19 (lift (S O)
+O x1) Appl)) (lift (S O) O (THead (Flat Appl) x1 x2)) (lift_head (Flat Appl)
+x1 x2 (S O) O)) c (drop_drop (Bind b) O c c (drop_refl c) t1))) H18))) t3
+H14))))))) H13)) (\lambda (H13: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) t1 x0) (THead (Bind
+Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: