dependences update

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/props.ma
index bccbf916947b9ca59d227e6070224d7828ceb08d..5da05fa2ad5e5a13e50f88a54e536139e3271600 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst0/fwd.ma".
+include "Basic-1/subst0/fwd.ma".
 
 theorem subst0_refl:
  \forall (u: T).(\forall (t: T).(\forall (d: nat).((subst0 d u t t) \to 
@@ -74,6 +74,9 @@ t0 x0)).(let H9 \def (eq_ind_r T x1 (\lambda (t2: T).(subst0 (s k d) u t1
 t2)) H5 t1 H7) in (let H10 \def (eq_ind_r T x0 (\lambda (t2: T).(subst0 d u 
 t0 t2)) H4 t0 H8) in (H d H10 P))))) H6))))))) H2)) (subst0_gen_head k u t0 
 t1 (THead k t0 t1) d H1)))))))))) t)).
+(* COMMENTS
+Initial nodes: 1119
+END *)
 
 theorem subst0_lift_lt:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -144,6 +147,9 @@ k i0) (lift h n v) (lift h (s k d) t0) (lift h (s k d) t3))) (H5 (s k d)
 (s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d 
 (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0)) 
 (lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1805
+END *)
 
 theorem subst0_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall 
@@ -202,6 +208,9 @@ h (s k d) t3)) (\lambda (t: T).(subst0 (plus i0 h) v (THead k (lift h d u1)
 h) (H1 d H4) k (lift h (s k d) t0) (lift h (s k d) t3) (H5 (s k d) (s_le k d 
 i0 H4))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead 
 k u1 t0)) (lift_head k u1 t0 h d)))))))))))))))) i u t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 1449
+END *)
 
 theorem subst0_lift_ge_S:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -214,6 +223,9 @@ t1) (lift (S O) d t2))))))))
 t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O) 
 i) (\lambda (n: nat).(eq nat n (S i))) (refl_equal nat (S i)) (plus i (S O)) 
 (plus_sym i (S O)))))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
 
 theorem subst0_lift_ge_s:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -223,4 +235,7 @@ i u t1 t2) \to (\forall (d: nat).((le d i) \to (\forall (b: B).(subst0 (s
  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda 
 (H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(\lambda 
 (_: B).(subst0_lift_ge_S t1 t2 u i H d H0)))))))).
+(* COMMENTS
+Initial nodes: 43
+END *)