-y2) z1 z2))))))) (pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O
-v1) t)) u2) (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
-T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H4: (not (eq B x0
-Abst))).(\lambda (H5: (pr3 c (THead (Bind b) v2 t) (THead (Bind x0) x1
-x2))).(\lambda (H6: (pr3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O)
-O x4) x3)) u2)).(\lambda (H7: (pr3 c v1 x4)).(\lambda (H8: (pr3 c x1
-x5)).(\lambda (H9: (pr3 (CHead c (Bind x0) x5) x2 x3)).(pr3_t (THead (Bind
-x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) (THead (Bind b) v2 (THead
-(Flat Appl) (lift (S O) O v1) t)) c (let H_x \def (pr3_gen_bind b H c v2 t
-(THead (Bind x0) x1 x2) H5) in (let H10 \def H_x in (or_ind (ex3_2 T T
-(\lambda (u3: T).(\lambda (t2: T).(eq T (THead (Bind x0) x1 x2) (THead (Bind
-b) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c v2 u3))) (\lambda (_:
-T).(\lambda (t2: T).(pr3 (CHead c (Bind b) v2) t t2)))) (pr3 (CHead c (Bind
-b) v2) t (lift (S O) O (THead (Bind x0) x1 x2))) (pr3 c (THead (Bind b) v2
-(THead (Flat Appl) (lift (S O) O v1) t)) (THead (Bind x0) x5 (THead (Flat
-Appl) (lift (S O) O x4) x3))) (\lambda (H11: (ex3_2 T T (\lambda (u3:
-T).(\lambda (t2: T).(eq T (THead (Bind x0) x1 x2) (THead (Bind b) u3 t2))))
-(\lambda (u3: T).(\lambda (_: T).(pr3 c v2 u3))) (\lambda (_: T).(\lambda
-(t2: T).(pr3 (CHead c (Bind b) v2) t t2))))).(ex3_2_ind T T (\lambda (u3:
-T).(\lambda (t2: T).(eq T (THead (Bind x0) x1 x2) (THead (Bind b) u3 t2))))
-(\lambda (u3: T).(\lambda (_: T).(pr3 c v2 u3))) (\lambda (_: T).(\lambda
-(t2: T).(pr3 (CHead c (Bind b) v2) t t2))) (pr3 c (THead (Bind b) v2 (THead
-(Flat Appl) (lift (S O) O v1) t)) (THead (Bind x0) x5 (THead (Flat Appl)
-(lift (S O) O x4) x3))) (\lambda (x6: T).(\lambda (x7: T).(\lambda (H12: (eq
-T (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7))).(\lambda (H13: (pr3 c v2
-x6)).(\lambda (H14: (pr3 (CHead c (Bind b) v2) t x7)).(let H15 \def (f_equal
-T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with [(TSort _)
-\Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead k _ _) \Rightarrow (match
-k in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow x0])])) (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7) H12) in
-((let H16 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
-T).T) with [(TSort _) \Rightarrow x1 | (TLRef _) \Rightarrow x1 | (THead _ t0
-_) \Rightarrow t0])) (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7) H12) in
-((let H17 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
-T).T) with [(TSort _) \Rightarrow x2 | (TLRef _) \Rightarrow x2 | (THead _ _
-t0) \Rightarrow t0])) (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7) H12) in
-(\lambda (H18: (eq T x1 x6)).(\lambda (H19: (eq B x0 b)).(let H20 \def
-(eq_ind_r T x7 (\lambda (t0: T).(pr3 (CHead c (Bind b) v2) t t0)) H14 x2 H17)
-in (let H21 \def (eq_ind_r T x6 (\lambda (t0: T).(pr3 c v2 t0)) H13 x1 H18)
-in (let H22 \def (eq_ind B x0 (\lambda (b0: B).(pr3 (CHead c (Bind b0) x5) x2
-x3)) H9 b H19) in (let H23 \def (eq_ind B x0 (\lambda (b0: B).(not (eq B b0
-Abst))) H4 b H19) in (eq_ind_r B b (\lambda (b0: B).(pr3 c (THead (Bind b) v2
-(THead (Flat Appl) (lift (S O) O v1) t)) (THead (Bind b0) x5 (THead (Flat
-Appl) (lift (S O) O x4) x3)))) (pr3_head_21 c v2 x5 (pr3_t x1 v2 c H21 x5 H8)
-(Bind b) (THead (Flat Appl) (lift (S O) O v1) t) (THead (Flat Appl) (lift (S
-O) O x4) x3) (pr3_flat (CHead c (Bind b) v2) (lift (S O) O v1) (lift (S O) O
-x4) (pr3_lift (CHead c (Bind b) v2) c (S O) O (drop_drop (Bind b) O c c
-(drop_refl c) v2) v1 x4 H7) t x3 (pr3_t x2 t (CHead c (Bind b) v2) H20 x3
+y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b0: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
+b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THead (Bind b) v2 t) (THead
+(Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (z2: T).(\lambda (u3: T).(\lambda (y2: T).(pr3 c (THead (Bind b0)
+y2 (THead (Flat Appl) (lift (S O) O u3) z2)) u2))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u3: T).(\lambda
+(_: T).(pr3 c v1 u3))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
+(\lambda (b0: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
+(_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b0) y2) z1 z2))))))) (pr3 c
+(THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) u2) (\lambda (x0:
+B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (x5: T).(\lambda (H4: (not (eq B x0 Abst))).(\lambda (H5: (pr3 c
+(THead (Bind b) v2 t) (THead (Bind x0) x1 x2))).(\lambda (H6: (pr3 c (THead
+(Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) u2)).(\lambda (H7:
+(pr3 c v1 x4)).(\lambda (H8: (pr3 c x1 x5)).(\lambda (H9: (pr3 (CHead c (Bind
+x0) x5) x2 x3)).(pr3_t (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O
+x4) x3)) (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) c (let
+H_x \def (pr3_gen_bind b H c v2 t (THead (Bind x0) x1 x2) H5) in (let H10
+\def H_x in (or_ind (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead
+(Bind x0) x1 x2) (THead (Bind b) u3 t2)))) (\lambda (u3: T).(\lambda (_:
+T).(pr3 c v2 u3))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind b)
+v2) t t2)))) (pr3 (CHead c (Bind b) v2) t (lift (S O) O (THead (Bind x0) x1
+x2))) (pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t))
+(THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))) (\lambda (H11:
+(ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead (Bind x0) x1 x2)
+(THead (Bind b) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c v2 u3)))
+(\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind b) v2) t
+t2))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead (Bind
+x0) x1 x2) (THead (Bind b) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c
+v2 u3))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind b) v2) t t2)))
+(pr3 c (THead (Bind b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) (THead
+(Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))) (\lambda (x6:
+T).(\lambda (x7: T).(\lambda (H12: (eq T (THead (Bind x0) x1 x2) (THead (Bind
+b) x6 x7))).(\lambda (H13: (pr3 c v2 x6)).(\lambda (H14: (pr3 (CHead c (Bind
+b) v2) t x7)).(let H15 \def (f_equal T B (\lambda (e: T).(match e with
+[(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead k _ _)
+\Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow
+x0])])) (THead (Bind x0) x1 x2) (THead (Bind b) x6 x7) H12) in ((let H16 \def
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x1 | (TLRef
+_) \Rightarrow x1 | (THead _ t0 _) \Rightarrow t0])) (THead (Bind x0) x1 x2)
+(THead (Bind b) x6 x7) H12) in ((let H17 \def (f_equal T T (\lambda (e:
+T).(match e with [(TSort _) \Rightarrow x2 | (TLRef _) \Rightarrow x2 |
+(THead _ _ t0) \Rightarrow t0])) (THead (Bind x0) x1 x2) (THead (Bind b) x6
+x7) H12) in (\lambda (H18: (eq T x1 x6)).(\lambda (H19: (eq B x0 b)).(let H20
+\def (eq_ind_r T x7 (\lambda (t0: T).(pr3 (CHead c (Bind b) v2) t t0)) H14 x2
+H17) in (let H21 \def (eq_ind_r T x6 (\lambda (t0: T).(pr3 c v2 t0)) H13 x1
+H18) in (let H22 \def (eq_ind B x0 (\lambda (b0: B).(pr3 (CHead c (Bind b0)
+x5) x2 x3)) H9 b H19) in (let H23 \def (eq_ind B x0 (\lambda (b0: B).(not (eq
+B b0 Abst))) H4 b H19) in (eq_ind_r B b (\lambda (b0: B).(pr3 c (THead (Bind
+b) v2 (THead (Flat Appl) (lift (S O) O v1) t)) (THead (Bind b0) x5 (THead
+(Flat Appl) (lift (S O) O x4) x3)))) (pr3_head_21 c v2 x5 (pr3_t x1 v2 c H21
+x5 H8) (Bind b) (THead (Flat Appl) (lift (S O) O v1) t) (THead (Flat Appl)
+(lift (S O) O x4) x3) (pr3_flat (CHead c (Bind b) v2) (lift (S O) O v1) (lift
+(S O) O x4) (pr3_lift (CHead c (Bind b) v2) c (S O) O (drop_drop (Bind b) O c
+c (drop_refl c) v2) v1 x4 H7) t x3 (pr3_t x2 t (CHead c (Bind b) v2) H20 x3