X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fty3%2Fdec.ma;h=7b2c899d70b58c383ea00ab56f025640a422395f;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=c176d635e627ec621d1af035589828002222cfad;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/dec.ma
index c176d635e..7b2c899d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/dec.ma
@@ -14,13 +14,15 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pc3/dec.ma".
+include "basic_1/pc3/dec.ma".
 
-include "Basic-1/getl/flt.ma".
+include "basic_1/getl/flt.ma".
 
-include "Basic-1/getl/dec.ma".
+include "basic_1/getl/dec.ma".
 
-theorem ty3_inference:
+include "basic_1/flt/fwd.ma".
+
+lemma ty3_inference:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2: 
 T).(ty3 g c t1 t2))) (\forall (t2: T).((ty3 g c t1 t2) \to False)))))
 \def
@@ -87,35 +89,101 @@ 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 False 
-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 
-(\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)))) False (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: 
-(pc3 c2 (lift (S n) O x4) t3)).(\lambda (H10: (getl n c2 (CHead x3 (Bind 
-Abst) 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 Abst) x4) 
+ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k 
+with [(Bind b) \Rightarrow (match b 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 False 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 (\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)))) False 
+(\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift 
+(S n) O x4) t3)).(\lambda (H10: (getl n c2 (CHead x3 (Bind Abst) 
+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 Abst) x4) 
 (getl_mono c2 (CHead x0 (Bind Void) x2) n H6 (CHead x3 (Bind Abst) 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 Abst) x4) (getl_mono c2 (CHead x0 
-(Bind Void) x2) n H6 (CHead x3 (Bind Abst) x4) H10)) in (False_ind False 
-H13))))))))) H8)) (ty3_gen_lref g c2 t3 n H7)))))) x1 H2))) H4)) (\lambda 
-(H4: ((\forall (t3: T).((ty3 g x0 x2 t3) \to False)))).(or_intror (ex T 
-(\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef 
-n) t3) \to False)) (\lambda (t3: T).(\lambda (H5: (ty3 g c2 (TLRef n) 
+ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k 
+with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow False | Abst 
+\Rightarrow False | Void \Rightarrow True]) | (Flat _) \Rightarrow False])])) 
+I (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind Void) x2) n H6 
+(CHead x3 (Bind Abst) x4) H10)) in (False_ind False H13))))))))) H8)) 
+(ty3_gen_lref g c2 t3 n H7)))))) x1 H2))) H4)) (\lambda (H4: ((\forall (t3: 
+T).((ty3 g x0 x2 t3) \to False)))).(or_intror (ex T (\lambda (t3: T).(ty3 g 
+c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to False)) 
+(\lambda (t3: T).(\lambda (H5: (ty3 g c2 (TLRef n) t3)).(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))))) False (\lambda (H6: (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)))) False (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: 
+(pc3 c2 (lift (S n) O x5) t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abbr) 
+x4))).(\lambda (H9: (ty3 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind 
+x1) x2) (\lambda (c0: C).(getl n c2 c0)) H2 (CHead x3 (Bind Abbr) x4) 
+(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in 
+(let H11 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) (CHead x0 (Bind x1) x2) 
+(CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead 
+x3 (Bind Abbr) x4) H8)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match 
+e with [(CSort _) \Rightarrow x1 | (CHead _ k _) \Rightarrow (match k with 
+[(Bind b) \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 (Bind x1) 
+x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 
+(CHead x3 (Bind Abbr) x4) H8)) in ((let H13 \def (f_equal C T (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow x2 | (CHead _ _ t) \Rightarrow t])) 
+(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 
+(Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in (\lambda (_: (eq B x1 
+Abbr)).(\lambda (H15: (eq C x0 x3)).(let H16 \def (eq_ind_r T x4 (\lambda (t: 
+T).(getl n c2 (CHead x3 (Bind Abbr) t))) H10 x2 H13) in (let H17 \def 
+(eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) H9 x2 H13) in (let H18 \def 
+(eq_ind_r C x3 (\lambda (c0: C).(getl n c2 (CHead c0 (Bind Abbr) x2))) H16 x0 
+H15) in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(ty3 g c0 x2 x5)) H17 
+x0 H15) in (H4 x5 H19)))))))) H12)) H11))))))))) H6)) (\lambda (H6: (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 (\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)))) False (\lambda (x3: C).(\lambda (x4: 
+T).(\lambda (x5: T).(\lambda (H7: (pc3 c2 (lift (S n) O x4) t3)).(\lambda 
+(H8: (getl n c2 (CHead x3 (Bind Abst) x4))).(\lambda (H9: (ty3 g x3 x4 
+x5)).(let H10 \def (eq_ind C (CHead x0 (Bind x1) x2) (\lambda (c0: C).(getl n 
+c2 c0)) H2 (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n 
+H2 (CHead x3 (Bind Abst) x4) H8)) in (let H11 \def (f_equal C C (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) 
+(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 
+(Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H12 \def (f_equal 
+C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow x1 | (CHead _ k _) 
+\Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow 
+x1])])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 
+(CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H13 \def 
+(f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow x2 | (CHead 
+_ _ t) \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) 
+(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in 
+(\lambda (_: (eq B x1 Abst)).(\lambda (H15: (eq C x0 x3)).(let H16 \def 
+(eq_ind_r T x4 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abst) t))) H10 x2 
+H13) in (let H17 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) H9 x2 
+H13) in (let H18 \def (eq_ind_r T x4 (\lambda (t: T).(pc3 c2 (lift (S n) O t) 
+t3)) H7 x2 H13) in (let H19 \def (eq_ind_r C x3 (\lambda (c0: C).(getl n c2 
+(CHead c0 (Bind Abst) x2))) H16 x0 H15) in (let H20 \def (eq_ind_r C x3 
+(\lambda (c0: C).(ty3 g c0 x2 x5)) H17 x0 H15) in (H4 x5 H20))))))))) H12)) 
+H11))))))))) H6)) (ty3_gen_lref g c2 t3 n H5)))))) H3)))))) H1)) (\lambda 
+(H1: ((\forall (d: C).((getl n c2 d) \to (\forall (P: Prop).P))))).(or_intror 
+(ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) (\forall (t3: T).((ty3 g c2 
+(TLRef n) t3) \to False)) (\lambda (t3: T).(\lambda (H2: (ty3 g c2 (TLRef n) 
 t3)).(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: 
@@ -123,87 +191,15 @@ 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))))) False 
-(\lambda (H6: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
+(\lambda (H3: (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)))) False 
-(\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (pc3 c2 (lift 
-(S n) O x5) t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abbr) 
-x4))).(\lambda (H9: (ty3 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind 
-x1) x2) (\lambda (c0: C).(getl n c2 c0)) H2 (CHead x3 (Bind Abbr) x4) 
-(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in 
-(let H11 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: 
-C).C) with [(CSort _) \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) 
-(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 
-(Bind x1) x2) n H2 (CHead x3 (Bind Abbr) x4) H8)) in ((let H12 \def (f_equal 
-C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) 
-\Rightarrow x1 | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: 
-K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 
-(Bind x1) x2) (CHead x3 (Bind Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) 
-n H2 (CHead x3 (Bind Abbr) x4) H8)) in ((let H13 \def (f_equal C T (\lambda 
-(e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2 
-| (CHead _ _ t) \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind 
-Abbr) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abbr) 
-x4) H8)) in (\lambda (_: (eq B x1 Abbr)).(\lambda (H15: (eq C x0 x3)).(let 
-H16 \def (eq_ind_r T x4 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abbr) t))) 
-H10 x2 H13) in (let H17 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) 
-H9 x2 H13) in (let H18 \def (eq_ind_r C x3 (\lambda (c0: C).(getl n c2 (CHead 
-c0 (Bind Abbr) x2))) H16 x0 H15) in (let H19 \def (eq_ind_r C x3 (\lambda 
-(c0: C).(ty3 g c0 x2 x5)) H17 x0 H15) in (H4 x5 H19)))))))) H12)) 
-H11))))))))) H6)) (\lambda (H6: (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 
-(\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)))) False (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H7: 
-(pc3 c2 (lift (S n) O x4) t3)).(\lambda (H8: (getl n c2 (CHead x3 (Bind Abst) 
-x4))).(\lambda (H9: (ty3 g x3 x4 x5)).(let H10 \def (eq_ind C (CHead x0 (Bind 
-x1) x2) (\lambda (c0: C).(getl n c2 c0)) H2 (CHead x3 (Bind Abst) x4) 
-(getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in 
-(let H11 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: 
-C).C) with [(CSort _) \Rightarrow x0 | (CHead c0 _ _) \Rightarrow c0])) 
-(CHead x0 (Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 
-(Bind x1) x2) n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H12 \def (f_equal 
-C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) 
-\Rightarrow x1 | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: 
-K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow x1])])) (CHead x0 
-(Bind x1) x2) (CHead x3 (Bind Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) 
-n H2 (CHead x3 (Bind Abst) x4) H8)) in ((let H13 \def (f_equal C T (\lambda 
-(e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow x2 
-| (CHead _ _ t) \Rightarrow t])) (CHead x0 (Bind x1) x2) (CHead x3 (Bind 
-Abst) x4) (getl_mono c2 (CHead x0 (Bind x1) x2) n H2 (CHead x3 (Bind Abst) 
-x4) H8)) in (\lambda (_: (eq B x1 Abst)).(\lambda (H15: (eq C x0 x3)).(let 
-H16 \def (eq_ind_r T x4 (\lambda (t: T).(getl n c2 (CHead x3 (Bind Abst) t))) 
-H10 x2 H13) in (let H17 \def (eq_ind_r T x4 (\lambda (t: T).(ty3 g x3 t x5)) 
-H9 x2 H13) in (let H18 \def (eq_ind_r T x4 (\lambda (t: T).(pc3 c2 (lift (S 
-n) O t) t3)) H7 x2 H13) in (let H19 \def (eq_ind_r C x3 (\lambda (c0: 
-C).(getl n c2 (CHead c0 (Bind Abst) x2))) H16 x0 H15) in (let H20 \def 
-(eq_ind_r C x3 (\lambda (c0: C).(ty3 g c0 x2 x5)) H17 x0 H15) in (H4 x5 
-H20))))))))) H12)) H11))))))))) H6)) (ty3_gen_lref g c2 t3 n H5)))))) 
-H3)))))) H1)) (\lambda (H1: ((\forall (d: C).((getl n c2 d) \to (\forall (P: 
-Prop).P))))).(or_intror (ex T (\lambda (t3: T).(ty3 g c2 (TLRef n) t3))) 
-(\forall (t3: T).((ty3 g c2 (TLRef n) t3) \to False)) (\lambda (t3: 
-T).(\lambda (H2: (ty3 g c2 (TLRef n) t3)).(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))))) False (\lambda (H3: (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)))) False (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: 
-(pc3 c2 (lift (S n) O x2) t3)).(\lambda (H5: (getl n c2 (CHead x0 (Bind Abbr) 
+(\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c2 (lift 
+(S n) O x2) t3)).(\lambda (H5: (getl n c2 (CHead x0 (Bind Abbr) 
 x1))).(\lambda (_: (ty3 g x0 x1 x2)).(H1 (CHead x0 (Bind Abbr) x1) H5 
 False))))))) H3)) (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (u: 
 T).(\lambda (_: T).(pc3 c2 (lift (S n) O u) t3)))) (\lambda (e: C).(\lambda 
@@ -432,7 +428,4 @@ t3)).(ex3_ind T (\lambda (t4: T).(pc3 c2 (THead (Flat Cast) t4 t) t3))
 T).(ty3 g c2 x0 t4)) False (\lambda (x: T).(\lambda (_: (ty3 g c2 x0 x)).(H5 
 x0 H9))) (ty3_correct g c2 t x0 H9)))))) (ty3_gen_cast g c2 t0 t t3 H6)))))) 
 H4))) f H2))) k H1))))))) t2))) c t1))).
-(* COMMENTS
-Initial nodes: 9001
-END *)