dependences update

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/next_plus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/next_plus/props.ma
index 7e26f27a7f902769562d09c93f0d75d4fefb044f..258c3a711bacce875591a3b84bc4df205d0f9e68 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/next_plus/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/next_plus/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/next_plus/defs.ma".
+include "Basic-1/next_plus/defs.ma".
 
 theorem next_plus_assoc:
  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq 
@@ -35,6 +35,9 @@ n0)) n1) (next g (next_plus g n (plus n0 n1))))).(eq_ind nat (S (plus n0 n1))
 n1)) (next g (next_plus g n n2)))) (f_equal nat nat (next g) (next_plus g 
 (next g (next_plus g n n0)) n1) (next g (next_plus g n (plus n0 n1))) H0) 
 (plus n0 (S n1)) (plus_n_Sm n0 n1)))) h2)))) h1))).
+(* COMMENTS
+Initial nodes: 351
+END *)
 
 theorem next_plus_next:
  \forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g 
@@ -44,6 +47,9 @@ theorem next_plus_next:
 g n (plus (S O) h)) (\lambda (n0: nat).(eq nat n0 (next g (next_plus g n 
 h)))) (refl_equal nat (next g (next_plus g n h))) (next_plus g (next_plus g n 
 (S O)) h) (next_plus_assoc g n (S O) h)))).
+(* COMMENTS
+Initial nodes: 87
+END *)
 
 theorem next_plus_lt:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next 
@@ -56,4 +62,7 @@ g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0))
 n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
 g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
 g n0) n)) (next_plus_next g (next g n0) n))))) h)).
+(* COMMENTS
+Initial nodes: 153
+END *)