(* 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".
+
+include "basic_1/flt/fwd.ma".
theorem ty3_inference:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2:
(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:
(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
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 *)