(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/arity".
+include "LambdaDelta-1/nf2/fwd.ma".
-include "nf2/fwd.ma".
-
-include "arity/subst0.ma".
+include "LambdaDelta-1/arity/subst0.ma".
theorem arity_nf2_inv_all:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
(TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 (CHead c0 (Bind
Abst) u) ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 (CHead c0 (Bind
Abst) u) (TLRef i))))))))).(\lambda (H4: (nf2 c0 (THead (Bind Abst) u
-t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2
+t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2
(CHead c0 (Bind Abst) u) t0) (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0:
T).(eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)))) (\lambda (w:
T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead
t0 (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
i))))))))).(\lambda (H4: (nf2 c0 (THead (Flat Appl) u t0))).(let H5 \def
-(nf2_gen_flat Appl c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2 c0 t0) (or3 (ex3_2
-T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead
-(Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda
-(w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda
-(n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList nat
-(\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0) (THeads
-(Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0
-ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i)))))) (\lambda
-(H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def (H3 H7) in (let H8
-\def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T t0
+(nf2_gen_flat Appl c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2 c0 t0) (or3
+(ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0)
(THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w)))
(\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat
-(\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat (\lambda (ws:
-TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
+(\lambda (n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList
+nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0)
+(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
+nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
+i)))))) (\lambda (H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def
+(H3 H7) in (let H8 \def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda
+(u0: T).(eq T t0 (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_:
+T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst)
+w) u0)))) (ex nat (\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat
+(\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef
+i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))) (or3 (ex3_2 T T (\lambda (w:
T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w
u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda
(THead (Flat Appl) u t1) (TSort n)))) (ex3_2 TList nat (\lambda (ws:
TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t1) (THeads (Flat Appl)
ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws)))
-(\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))))) (let H13 \def
-(match (arity_gen_sort g c0 x (AHead a1 a2) H12) in leq return (\lambda (a0:
-A).(\lambda (a3: A).(\lambda (_: (leq ? a0 a3)).((eq A a0 (AHead a1 a2)) \to
-((eq A a3 (ASort O x)) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0:
-T).(eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)))) (\lambda
-(w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2
-(CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda (n: nat).(eq T (THead (Flat
-Appl) u (TSort x)) (TSort n)))) (ex3_2 TList nat (\lambda (ws:
-TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u (TSort x)) (THeads (Flat
-Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws)))
-(\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))))))))) with
-[(leq_sort h1 h2 n1 n2 k H13) \Rightarrow (\lambda (H14: (eq A (ASort h1 n1)
-(AHead a1 a2))).(\lambda (H15: (eq A (ASort h2 n2) (ASort O x))).((let H16
-\def (eq_ind A (ASort h1 n1) (\lambda (e: A).(match e in A return (\lambda
-(_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _) \Rightarrow
-False])) I (AHead a1 a2) H14) in (False_ind ((eq A (ASort h2 n2) (ASort O x))
-\to ((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (or3
-(ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u (TSort
-x)) (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w)))
-(\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat
-(\lambda (n: nat).(eq T (THead (Flat Appl) u (TSort x)) (TSort n)))) (ex3_2
-TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u
-(TSort x)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda
-(_: nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
-i)))))))) H16)) H15 H13))) | (leq_head a0 a3 H13 a4 a5 H14) \Rightarrow
-(\lambda (H15: (eq A (AHead a0 a4) (AHead a1 a2))).(\lambda (H16: (eq A
-(AHead a3 a5) (ASort O x))).((let H17 \def (f_equal A A (\lambda (e:
-A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 |
-(AHead _ a6) \Rightarrow a6])) (AHead a0 a4) (AHead a1 a2) H15) in ((let H18
-\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
-with [(ASort _ _) \Rightarrow a0 | (AHead a6 _) \Rightarrow a6])) (AHead a0
-a4) (AHead a1 a2) H15) in (eq_ind A a1 (\lambda (a6: A).((eq A a4 a2) \to
-((eq A (AHead a3 a5) (ASort O x)) \to ((leq g a6 a3) \to ((leq g a4 a5) \to
-(or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u
-(TSort x)) (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2
-c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0))))
-(ex nat (\lambda (n: nat).(eq T (THead (Flat Appl) u (TSort x)) (TSort n))))
-(ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat
-Appl) u (TSort x)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws:
-TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i:
-nat).(nf2 c0 (TLRef i))))))))))) (\lambda (H19: (eq A a4 a2)).(eq_ind A a2
-(\lambda (a6: A).((eq A (AHead a3 a5) (ASort O x)) \to ((leq g a1 a3) \to
-((leq g a6 a5) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T
-(THead (Flat Appl) u (TSort x)) (THead (Bind Abst) w u0)))) (\lambda (w:
-T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead
-c0 (Bind Abst) w) u0)))) (ex nat (\lambda (n: nat).(eq T (THead (Flat Appl) u
-(TSort x)) (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i:
-nat).(eq T (THead (Flat Appl) u (TSort x)) (THeads (Flat Appl) ws (TLRef
-i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
-TList).(\lambda (i: nat).(nf2 c0 (TLRef i)))))))))) (\lambda (H20: (eq A
-(AHead a3 a5) (ASort O x))).(let H21 \def (eq_ind A (AHead a3 a5) (\lambda
-(e: A).(match e in A return (\lambda (_: A).Prop) with [(ASort _ _)
-\Rightarrow False | (AHead _ _) \Rightarrow True])) I (ASort O x) H20) in
-(False_ind ((leq g a1 a3) \to ((leq g a2 a5) \to (or3 (ex3_2 T T (\lambda (w:
-T).(\lambda (u0: T).(eq T (THead (Flat Appl) u (TSort x)) (THead (Bind Abst)
-w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w:
-T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda (n:
-nat).(eq T (THead (Flat Appl) u (TSort x)) (TSort n)))) (ex3_2 TList nat
+(\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))))) (let H_x0 \def
+(leq_gen_head1 g a1 a2 (ASort O x) (arity_gen_sort g c0 x (AHead a1 a2) H12))
+in (let H13 \def H_x0 in (ex3_2_ind A A (\lambda (a3: A).(\lambda (_: A).(leq
+g a1 a3))) (\lambda (_: A).(\lambda (a4: A).(leq g a2 a4))) (\lambda (a3:
+A).(\lambda (a4: A).(eq A (ASort O x) (AHead a3 a4)))) (or3 (ex3_2 T T
+(\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u (TSort x)) (THead
+(Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda
+(w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda
+(n: nat).(eq T (THead (Flat Appl) u (TSort x)) (TSort n)))) (ex3_2 TList nat
(\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u (TSort x))
(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
-i)))))))) H21))) a4 (sym_eq A a4 a2 H19))) a0 (sym_eq A a0 a1 H18))) H17))
-H16 H13 H14)))]) in (H13 (refl_equal A (AHead a1 a2)) (refl_equal A (ASort O
-x)))) t0 H10))))) H9)) (\lambda (H9: (ex3_2 TList nat (\lambda (ws:
-TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
+i)))))) (\lambda (x0: A).(\lambda (x1: A).(\lambda (_: (leq g a1
+x0)).(\lambda (_: (leq g a2 x1)).(\lambda (H16: (eq A (ASort O x) (AHead x0
+x1))).(let H17 \def (eq_ind A (ASort O x) (\lambda (ee: A).(match ee in A
+return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow True | (AHead _ _)
+\Rightarrow False])) I (AHead x0 x1) H16) in (False_ind (or3 (ex3_2 T T
+(\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u (TSort x)) (THead
+(Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda
+(w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda
+(n: nat).(eq T (THead (Flat Appl) u (TSort x)) (TSort n)))) (ex3_2 TList nat
+(\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u (TSort x))
+(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
+nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
+i)))))) H17))))))) H13))) t0 H10))))) H9)) (\lambda (H9: (ex3_2 TList nat
+(\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef
+i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
TList).(\lambda (i: nat).(nf2 c0 (TLRef i)))))).(ex3_2_ind TList nat (\lambda
(ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_: