dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / ty3 / arity_props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/arity_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/arity_props.ma
index 5357e58e25c43f17698a5b6405165186f3bcba09..49d6c0572716f872324c2ea57f92df9fa89443b3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/arity_props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/arity_props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/arity.ma".
+include "Basic-1/ty3/arity.ma".
 
-include "LambdaDelta-1/sc3/arity.ma".
+include "Basic-1/sc3/arity.ma".
 
 theorem ty3_predicative:
  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u: 
@@ -46,6 +46,9 @@ x2))).(\lambda (_: (arity g (CHead c (Bind Abst) v) t x3)).(let H12 \def
 in (leq_ahead_asucc_false g x2 (asucc g x3) (arity_mono g c v (asucc g (AHead 
 x2 x3)) H12 (asucc g x2) H10) P))))))) H8))))) H5))))))))) (ty3_gen_bind g 
 Abst c v t u H1)))))))))).
+(* COMMENTS
+Initial nodes: 497
+END *)
 
 theorem ty3_repellent:
  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (t: T).(\forall (u1: 
@@ -79,6 +82,9 @@ c u2 (asucc g x1) (arity_gen_lift g (CHead c (Bind Abst) w) u2 (asucc g x1)
 (S O) O H8 c (drop_drop (Bind Abst) O c c (drop_refl c) w)) (asucc g x2) 
 H11)) P)))) H9)))))) H6))))))) H3)))) (ty3_correct g (CHead c (Bind Abst) w) 
 t (lift (S O) O u2) H0))))))))))).
+(* COMMENTS
+Initial nodes: 651
+END *)
 
 theorem ty3_acyclic:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
@@ -91,6 +97,9 @@ u) \to ((pc3 c u t) \to (\forall (P: Prop).P))))))
 (a1: A).(arity g c t (asucc g a1))) P (\lambda (x: A).(\lambda (H2: (arity g 
 c t x)).(\lambda (H3: (arity g c t (asucc g x))).(leq_asucc_false g x 
 (arity_mono g c t (asucc g x) H3 x H2) P)))) H1)))))))))).
+(* COMMENTS
+Initial nodes: 151
+END *)
 
 theorem ty3_sn3:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
@@ -102,4 +111,7 @@ u) \to (sn3 c t)))))
 (asucc g a1))) (sn3 c t) (\lambda (x: A).(\lambda (H1: (arity g c t 
 x)).(\lambda (_: (arity g c u (asucc g x))).(sc3_sn3 g x c t (sc3_arity g c t 
 x H1))))) H0))))))).
+(* COMMENTS
+Initial nodes: 119
+END *)