dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / leq / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/fwd.ma
index ddfce504d6ea73d945edd1d2f53877c28eb8a041..e259fa19e134290366ff5d14e1aefad6655dae07 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/leq/defs.ma".
+include "Basic-1/leq/defs.ma".
 
 theorem leq_gen_sort1:
  \forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq 
@@ -72,6 +72,9 @@ nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (AHead a1 a4) k)
 (aplus g (ASort h2 n2) k))))) (\lambda (n2: nat).(\lambda (h2: nat).(\lambda 
 (_: nat).(eq A (AHead a3 a5) (ASort h2 n2)))))) H6))))))))))) y a2 H0))) 
 H))))).
+(* COMMENTS
+Initial nodes: 913
+END *)
 
 theorem leq_gen_head1:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((leq g 
@@ -122,6 +125,9 @@ A (\lambda (a6: A).(\lambda (_: A).(leq g a1 a6))) (\lambda (_: A).(\lambda
 (a7: A).(leq g a2 a7))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a3 a5) 
 (AHead a6 a7)))) a3 a5 H12 H10 (refl_equal A (AHead a3 a5))))))))) 
 H6))))))))))) y a H0))) H))))).
+(* COMMENTS
+Initial nodes: 797
+END *)
 
 theorem leq_gen_sort2:
  \forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq 
@@ -179,6 +185,9 @@ nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (ASort h2 n2) k)
 (aplus g (AHead a3 a5) k))))) (\lambda (n2: nat).(\lambda (h2: nat).(\lambda 
 (_: nat).(eq A (AHead a1 a4) (ASort h2 n2)))))) H6))))))))))) a2 y H0))) 
 H))))).
+(* COMMENTS
+Initial nodes: 913
+END *)
 
 theorem leq_gen_head2:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((leq g a 
@@ -229,4 +238,7 @@ A (\lambda (a6: A).(\lambda (_: A).(leq g a6 a1))) (\lambda (_: A).(\lambda
 (a7: A).(leq g a7 a2))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a0 a4) 
 (AHead a6 a7)))) a0 a4 H12 H10 (refl_equal A (AHead a0 a4))))))))) 
 H6))))))))))) a y H0))) H))))).
+(* COMMENTS
+Initial nodes: 797
+END *)