(* This file was automatically generated: do not edit *********************)
-include "Basic-1/ty3/arity.ma".
+include "basic_1/ty3/arity.ma".
-include "Basic-1/pc3/nf2.ma".
+include "basic_1/pc3/nf2.ma".
-include "Basic-1/nf2/arity.ma".
+include "basic_1/nf2/arity.ma".
definition ty3_nf2_inv_abst_premise:
C \to (T \to (T \to Prop))
TList).((pc3 c (THeads (Flat Appl) vs (lift (S i) O wi)) (THead (Bind Abst) w
u)) \to False)))))))).
-theorem ty3_nf2_inv_abst_premise_csort:
+lemma ty3_nf2_inv_abst_premise_csort:
\forall (w: T).(\forall (u: T).(\forall (m: nat).(ty3_nf2_inv_abst_premise
(CSort m) w u)))
\def
wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs
(lift (S i) O wi)) (THead (Bind Abst) w u))).(getl_gen_sort m i (CHead d
(Bind Abst) wi) H False))))))))).
-(* COMMENTS
-Initial nodes: 85
-END *)
-theorem ty3_nf2_inv_all:
+lemma ty3_nf2_inv_all:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
u) \to ((nf2 c t) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T
t (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))
TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2:
(arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g
c t x H2 H0)))) H1)))))))).
-(* COMMENTS
-Initial nodes: 233
-END *)
-theorem ty3_nf2_inv_sort:
+lemma ty3_nf2_inv_sort:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
(TSort m)) \to ((nf2 c t) \to (or (ex2 nat (\lambda (n: nat).(eq T t (TSort
n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i))))
x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3)))))))
H2)) H1)))))))).
-(* COMMENTS
-Initial nodes: 2045
-END *)
-theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
+fact ty3_nf2_gen__ty3_nf2_inv_abst_aux:
\forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise
c w1 u1) \to (\forall (t: T).(\forall (w2: T).(\forall (u2: T).((pc3 c (THead
(Flat Appl) t (THead (Bind Abst) w2 u2)) (THead (Bind Abst) w1 u1)) \to
(THeads (Flat Appl) vs (lift (S i) O wi))) (pc3_thin_dx c (THeads (Flat Appl)
vs (lift (S i) O wi)) (THead (Bind Abst) w2 u2) H2 t Appl) (THead (Bind Abst)
w1 u1) H0))))))))))))))).
-(* COMMENTS
-Initial nodes: 271
-END *)
-theorem ty3_nf2_inv_abst:
+lemma ty3_nf2_inv_abst:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u:
T).((ty3 g c t (THead (Bind Abst) w u)) \to ((nf2 c t) \to ((nf2 c w) \to
((ty3_nf2_inv_abst_premise c w u) \to (ex4_2 T T (\lambda (v: T).(\lambda (_:
(Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind
Abst) x) v)))))) (\lambda (H22: (eq T (THeads (Flat Appl) TNil (TLRef x1))
(THead (Bind Abst) x3 x5))).(let H23 \def (eq_ind T (TLRef x1) (\lambda (ee:
-T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
-(THead (Bind Abst) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda (v:
-T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) TNil
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x) v))))
-H23))) (\lambda (t2: T).(\lambda (t3: TList).(\lambda (_: (((eq T (THeads
-(Flat Appl) t3 (TLRef x1)) (THead (Bind Abst) x3 x5)) \to (ex4_2 T T (\lambda
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) t3
-(TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0: T).(ty3
-g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) x) v
-x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
-v))))))).(\lambda (H22: (eq T (THeads (Flat Appl) (TCons t2 t3) (TLRef x1))
-(THead (Bind Abst) x3 x5))).(let H23 \def (eq_ind T (THead (Flat Appl) t2
-(THeads (Flat Appl) t3 (TLRef x1))) (\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 _) \Rightarrow False | (Flat _) \Rightarrow
-True])])) I (THead (Bind Abst) x3 x5) H22) in (False_ind (ex4_2 T T (\lambda
-(v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0 (THeads (Flat Appl) (TCons
-t2 t3) (TLRef x1))) (THead (Bind Abst) x v)))) (\lambda (_: T).(\lambda (w0:
-T).(ty3 g c x w0))) (\lambda (v: T).(\lambda (_: T).(ty3 g (CHead c (Bind
-Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
-v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat
-Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t
-H5))))))) H4)) H3))))))))))).
-(* COMMENTS
-Initial nodes: 5333
-END *)
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
+(THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x3 x5) H22) in
+(False_ind (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat
+Appl) t0 (THeads (Flat Appl) TNil (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23))) (\lambda (t2: T).(\lambda (t3:
+TList).(\lambda (_: (((eq T (THeads (Flat Appl) t3 (TLRef x1)) (THead (Bind
+Abst) x3 x5)) \to (ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead
+(Flat Appl) t0 (THeads (Flat Appl) t3 (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v))))))).(\lambda (H22: (eq T (THeads (Flat
+Appl) (TCons t2 t3) (TLRef x1)) (THead (Bind Abst) x3 x5))).(let H23 \def
+(eq_ind T (THead (Flat Appl) t2 (THeads (Flat Appl) t3 (TLRef x1))) (\lambda
+(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
+False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False |
+(Flat _) \Rightarrow True])])) I (THead (Bind Abst) x3 x5) H22) in (False_ind
+(ex4_2 T T (\lambda (v: T).(\lambda (_: T).(eq T (THead (Flat Appl) t0
+(THeads (Flat Appl) (TCons t2 t3) (TLRef x1))) (THead (Bind Abst) x v))))
+(\lambda (_: T).(\lambda (w0: T).(ty3 g c x w0))) (\lambda (v: T).(\lambda
+(_: T).(ty3 g (CHead c (Bind Abst) x) v x2))) (\lambda (v: T).(\lambda (_:
+T).(nf2 (CHead c (Bind Abst) x) v)))) H23)))))) t1 H18))))))) H17)))))))))
+(ty3_gen_appl g c t0 (THeads (Flat Appl) t1 (TLRef x1)) (THead (Bind Abst) x
+x2) H12))))))))) x0)) H10)) H9)) t H5))))))) H4)) H3))))))))))).