components/library: dotdothack removed

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / nf2 / arity.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
index 867f573e8f75beefa33173de8d2477e3be820078..0b17ee3784a311098a09ea7c46aa9d626092b70f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma
@@ -289,72 +289,33 @@ 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 (_: