-x)).((match x1 in B return (\lambda (b: B).((getl n c2 (CHead x0 (Bind b)
-x2)) \to (or (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3:
-T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))))) with [Abbr
-\Rightarrow (\lambda (H6: (getl n c2 (CHead x0 (Bind Abbr) x2))).(or_introl
-(ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2
-(TLRef n) t3) \to (\forall (P: Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g
-c2 (TLRef n) t3)) (lift (S n) O x) (ty3_abbr g n c2 x0 x2 H6 x H5)))) | Abst
-\Rightarrow (\lambda (H6: (getl n c2 (CHead x0 (Bind Abst) x2))).(or_introl
-(ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2
-(TLRef n) t3) \to (\forall (P: Prop).P))) (ex_intro T (\lambda (t3: T).(ty3 g
-c2 (TLRef n) t3)) (lift (S n) O x2) (ty3_abst g n c2 x0 x2 H6 x H5)))) | Void
-\Rightarrow (\lambda (H6: (getl n c2 (CHead x0 (Bind Void) x2))).(or_intror
-(ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2
-(TLRef n) t3) \to (\forall (P: Prop).P))) (\lambda (t3: T).(\lambda (H7: (ty3
-g c2 (TLRef n) t3)).(\lambda (P: Prop).(or_ind (ex3_3 C T T (\lambda (_:
-C).(\lambda (_: T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda
-(e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u)))))
-(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T
-T (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u)
-t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
-(Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
-t))))) P (\lambda (H8: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda
-(t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u:
-T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
-C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))).(ex3_3_ind C T T
-(\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c2 (lift (S n) O t)
-t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e
-(Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u
-t)))) P (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3
-c2 (lift (S n) O x5) t3)).(\lambda (H10: (getl n c2 (CHead x3 (Bind Abbr)
-x4))).(\lambda (_: (ty3 g x3 x4 x5)).(let H12 \def (eq_ind C (CHead x0 (Bind
-Void) x2) (\lambda (c0: C).(getl n c2 c0)) H6 (CHead x3 (Bind Abbr) x4)
-(getl_mono c2 (CHead x0 (Bind Void) x2) n H6 (CHead x3 (Bind Abbr) x4) H10))
-in (let H13 \def (eq_ind C (CHead x0 (Bind Void) x2) (\lambda (ee: C).(match
-ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
-(CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with
-[(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr
-\Rightarrow False | Abst \Rightarrow False | Void \Rightarrow True]) | (Flat
-_) \Rightarrow False])])) I (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0
-(Bind Void) x2) n H6 (CHead x3 (Bind Abbr) x4) H10)) in (False_ind P
-H13))))))))) H8)) (\lambda (H8: (ex3_3 C T T (\lambda (_: C).(\lambda (u:
-T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda
-(u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u))))) (\lambda (e:
-C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))))).(ex3_3_ind C T T
+x)).(B_ind (\lambda (b: B).((getl n c2 (CHead x0 (Bind b) x2)) \to (or (ex T
+(\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef
+n) t3) \to (\forall (P: Prop).P)))))) (\lambda (H6: (getl n c2 (CHead x0
+(Bind Abbr) x2))).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
+(\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
+(ex_intro T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)) (lift (S n) O x)
+(ty3_abbr g n c2 x0 x2 H6 x H5)))) (\lambda (H6: (getl n c2 (CHead x0 (Bind
+Abst) x2))).(or_introl (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
+(\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
+(ex_intro T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)) (lift (S n) O x2)
+(ty3_abst g n c2 x0 x2 H6 x H5)))) (\lambda (H6: (getl n c2 (CHead x0 (Bind
+Void) x2))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3)))
+(\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to (\forall (P: Prop).P)))
+(\lambda (t3: T).(\lambda (H7: (ty3 g c2 (TLRef n) t3)).(\lambda (P:
+Prop).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t:
+T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda
+(_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u:
+T).(\lambda (t: T).(ty3 g e u t))))) (ex3_3 C T T (\lambda (_: C).(\lambda
+(u: T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e:
+C).(\lambda (u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abst) u)))))
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t))))) P (\lambda
+(H8: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 c2
+(lift (S n) O t) t3)))) (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl
+n c2 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t:
+T).(ty3 g e u t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_:
+T).(\lambda (t: T).(pc3 c2 (lift (S n) O t) t3)))) (\lambda (e: C).(\lambda
+(u: T).(\lambda (_: T).(getl n c2 (CHead e (Bind Abbr) u))))) (\lambda (e:
+C).(\lambda (u: T).(\lambda (t: T).(ty3 g e u t)))) P (\lambda (x3:
+C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift (S n) O x5)
+t3)).(\lambda (H10: (getl n c2 (CHead x3 (Bind Abbr) x4))).(\lambda (_: (ty3
+g x3 x4 x5)).(let H12 \def (eq_ind C (CHead x0 (Bind Void) x2) (\lambda (c0:
+C).(getl n c2 c0)) H6 (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind
+Void) x2) n H6 (CHead x3 (Bind Abbr) x4) H10)) in (let H13 \def (eq_ind C
+(CHead x0 (Bind Void) x2) (\lambda (ee: C).(match ee in C return (\lambda (_:
+C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match
+k in K return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B
+return (\lambda (_: B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow
+False | Void \Rightarrow True]) | (Flat _) \Rightarrow False])])) I (CHead x3
+(Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind Void) x2) n H6 (CHead x3 (Bind
+Abbr) x4) H10)) in (False_ind P H13))))))))) H8)) (\lambda (H8: (ex3_3 C T T