dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / arity / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/props.ma
index 2e45247f2386e851c4055532d9ee3ef97a90b7d2..6f131df09a09547f7dd4753447560501cb6c8fe6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/arity/fwd.ma".
+include "Basic-1/arity/fwd.ma".
 
 theorem node_inh:
  \forall (g: G).(\forall (n: nat).(\forall (k: nat).(ex_2 C T (\lambda (c: 
@@ -32,6 +32,9 @@ T).(\lambda (H1: (arity g x0 x1 (ASort n0 n))).(ex_2_intro C T (\lambda (c:
 C).(\lambda (t: T).(arity g c t (ASort (S n0) n)))) (CHead x0 (Bind Abst) x1) 
 (TLRef O) (arity_abst g (CHead x0 (Bind Abst) x1) x0 x1 O (getl_refl Abst x0 
 x1) (ASort (S n0) n) H1))))) H0)))) k))).
+(* COMMENTS
+Initial nodes: 253
+END *)
 
 theorem arity_lift:
  \forall (g: G).(\forall (c2: C).(\forall (t: T).(\forall (a: A).((arity g c2 
@@ -152,6 +155,9 @@ a1))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c1:
 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H3: (drop h d c1 
 c)).(arity_repl g c1 (lift h d t0) a1 (H1 c1 h d H3) a2 H2)))))))))))) c2 t a 
 H))))).
+(* COMMENTS
+Initial nodes: 2661
+END *)
 
 theorem arity_mono:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a1: A).((arity g c 
@@ -301,6 +307,9 @@ a2)).(H3 a2 H7))) H5)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda
 A).((arity g c0 t0 a3) \to (leq g a2 a3))))).(\lambda (a3: A).(\lambda (H2: 
 (leq g a2 a3)).(\lambda (a0: A).(\lambda (H3: (arity g c0 t0 a0)).(leq_trans 
 g a3 a2 (leq_sym g a2 a3 H2) a0 (H1 a0 H3))))))))))) c t a1 H))))).
+(* COMMENTS
+Initial nodes: 2947
+END *)
 
 theorem arity_repellent:
  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (t: T).(\forall (a1: 
@@ -321,6 +330,9 @@ x0))).(\lambda (H5: (arity g (CHead c (Bind Abst) w) t x1)).(let H6 \def
 (eq_ind A a2 (\lambda (a: A).(arity g (CHead c (Bind Abst) w) t a)) H_y 
 (AHead x0 x1) H3) in (leq_ahead_false_2 g x1 x0 (arity_mono g (CHead c (Bind 
 Abst) w) t (AHead x0 x1) H6 x1 H5) P))))))) H2)))))))))))).
+(* COMMENTS
+Initial nodes: 283
+END *)
 
 theorem arity_appls_cast:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (vs: 
@@ -356,6 +368,9 @@ a)) (arity_repl g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g a)) H7
 (AHead x (asucc g a)) (leq_head g x0 x (arity_mono g c t0 x0 H6 x H3) (asucc 
 g a) (asucc g a) (leq_refl g (asucc g a)))) (asucc g (AHead x a)) (leq_refl g 
 (asucc g (AHead x a)))) H4))))) H5))))) H2)))))))) vs))))).
+(* COMMENTS
+Initial nodes: 707
+END *)
 
 theorem arity_appls_abbr:
  \forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
@@ -380,6 +395,9 @@ g c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) a) (\lambda (x:
 A).(\lambda (H3: (arity g c t x)).(\lambda (H4: (arity g c (THeads (Flat 
 Appl) t0 (lift (S i) O v)) (AHead x a))).(arity_appl g c t x H3 (THeads (Flat 
 Appl) t0 (TLRef i)) a (H0 (AHead x a) H4))))) H2))))))) vs))))))).
+(* COMMENTS
+Initial nodes: 425
+END *)
 
 theorem arity_appls_bind:
  \forall (g: G).(\forall (b: B).((not (eq B b Abst)) \to (\forall (c: 
@@ -410,4 +428,7 @@ g (CHead c (Bind b) v) (THeads (Flat Appl) (lifts (S O) O t1) t) (AHead x
 a2))).(arity_appl g c t0 x (arity_gen_lift g (CHead c (Bind b) v) t0 x (S O) 
 O H4 c (drop_drop (Bind b) O c c (drop_refl c) v)) (THeads (Flat Appl) t1 
 (THead (Bind b) v t)) a2 (H1 (AHead x a2) H5))))) H3))))))) vs))))))))).
+(* COMMENTS
+Initial nodes: 567
+END *)