-(THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
-[(Bind b0) \Rightarrow (match b0 in B return (\lambda (_: B).Prop) with [Abbr
-\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
-_) \Rightarrow False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3
-(CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2)))
-H14)))))))) H9))))))) H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1
-(lift (S O) O x))).(let H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T
-(\lambda (u3: T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3))))
-(\lambda (u3: T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda
-(t3: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2
-t3))))) (pc3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2
-t2))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind
-Abst) x0 x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0:
-B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def
-(eq_ind T x (\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O
-t))) H5 (THead (Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1)
-t1 (lift (S O) O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind
-Abst) u2 t2)) (pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind
-Abbr) O c c (drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0
-x1) (pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6)))
-H4))))) H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c:
-C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2:
-T).(\lambda (_: (pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2
-t2))).(let H1 \def (match (H (refl_equal B Abst)) in False return (\lambda
-(_: False).(pc3 (CHead c (Bind Abst) u1) t1 (lift (S O) O (THead (Bind Abst)
-u2 t2)))) with []) in H1)))))))) (\lambda (_: (not (eq B Void
-Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (u1:
-T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1) (THead
-(Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t: T).(pr3 c
-(THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2
-t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind Abst) u2
-t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1)
+(THead (Bind Abst) x2 x3) (\lambda (ee: T).(match ee with [(TSort _)
+\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow
+(match k with [(Bind b0) \Rightarrow (match b0 with [Abbr \Rightarrow False |
+Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow
+False])])) I (THead (Bind Abbr) x0 x1) H13) in (False_ind (pc3 (CHead c (Bind
+Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) H14)))))))) H9)))))))
+H5)) (\lambda (H5: (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x))).(let
+H6 \def (pr3_gen_abst c u2 t2 x H3) in (ex3_2_ind T T (\lambda (u3:
+T).(\lambda (t3: T).(eq T x (THead (Bind Abst) u3 t3)))) (\lambda (u3:
+T).(\lambda (_: T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall
+(b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t2 t3))))) (pc3 (CHead c
+(Bind Abbr) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))) (\lambda (x0:
+T).(\lambda (x1: T).(\lambda (H7: (eq T x (THead (Bind Abst) x0
+x1))).(\lambda (H8: (pr3 c u2 x0)).(\lambda (H9: ((\forall (b0: B).(\forall
+(u: T).(pr3 (CHead c (Bind b0) u) t2 x1))))).(let H10 \def (eq_ind T x
+(\lambda (t: T).(pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O t))) H5 (THead
+(Bind Abst) x0 x1) H7) in (pc3_pr3_t (CHead c (Bind Abbr) u1) t1 (lift (S O)
+O (THead (Bind Abst) x0 x1)) H10 (lift (S O) O (THead (Bind Abst) u2 t2))
+(pr3_lift (CHead c (Bind Abbr) u1) c (S O) O (drop_drop (Bind Abbr) O c c
+(drop_refl c) u1) (THead (Bind Abst) u2 t2) (THead (Bind Abst) x0 x1)
+(pr3_head_12 c u2 x0 H8 (Bind Abst) t2 x1 (H9 Abst x0)))))))))) H6))) H4)))))
+H1))))))))) (\lambda (H: (not (eq B Abst Abst))).(\lambda (c: C).(\lambda
+(t1: T).(\lambda (t2: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pc3
+c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2))).(let H1 \def (match
+(H (refl_equal B Abst)) in False with []) in H1)))))))) (\lambda (_: (not (eq
+B Void Abst))).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
+(u1: T).(\lambda (u2: T).(\lambda (H0: (pc3 c (THead (Bind Void) u1 t1)
+(THead (Bind Abst) u2 t2))).(let H1 \def H0 in (ex2_ind T (\lambda (t:
+T).(pr3 c (THead (Bind Void) u1 t1) t)) (\lambda (t: T).(pr3 c (THead (Bind
+Abst) u2 t2) t)) (pc3 (CHead c (Bind Void) u1) t1 (lift (S O) O (THead (Bind
+Abst) u2 t2))) (\lambda (x: T).(\lambda (H2: (pr3 c (THead (Bind Void) u1 t1)