uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/props.ma
index cb13ac64451b5dff408db314070afd7bd6802767..ac8dea954a58cf9a878caf8362c6b88de0fcaa10 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst1/defs.ma".
+include "Basic-1/subst1/defs.ma".
 
-include "LambdaDelta-1/subst0/props.ma".
+include "Basic-1/subst0/props.ma".
 
 theorem subst1_head:
  \forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1 
@@ -38,6 +38,9 @@ k u1 t1) (THead k t2 t))) (subst1_single i v (THead k u1 t1) (THead k t2 t1)
 (subst0_fst v t2 u1 i H0 t1 k)) (\lambda (t3: T).(\lambda (H2: (subst0 (s k 
 i) v t1 t3)).(subst1_single i v (THead k u1 t1) (THead k t2 t3) (subst0_both 
 v u1 t2 i H0 k t1 t3 H2)))) t0 H1))))))) u2 H))))).
+(* COMMENTS
+Initial nodes: 369
+END *)
 
 theorem subst1_lift_lt:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst1 
@@ -53,6 +56,9 @@ t1))))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda (d:
 nat).(\lambda (H1: (lt i d)).(\lambda (h: nat).(subst1_single i (lift h 
 (minus d (S i)) u) (lift h d t1) (lift h d t3) (subst0_lift_lt t1 t3 u i H0 d 
 H1 h))))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 185
+END *)
 
 theorem subst1_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall 
@@ -66,6 +72,9 @@ d t))))) (\lambda (d: nat).(\lambda (_: (le d i)).(subst1_refl (plus i h) u
 (lift h d t1)))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda 
 (d: nat).(\lambda (H1: (le d i)).(subst1_single (plus i h) u (lift h d t1) 
 (lift h d t3) (subst0_lift_ge t1 t3 u i h H0 d H1)))))) t2 H)))))).
+(* COMMENTS
+Initial nodes: 157
+END *)
 
 theorem subst1_ex:
  \forall (u: T).(\forall (t1: T).(\forall (d: nat).(ex T (\lambda (t2: 
@@ -106,6 +115,9 @@ t2))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x) (lift (S O) (s k
 d) x0)) (\lambda (t2: T).(subst1 d u (THead k t t0) t2)) (subst1_head u t 
 (lift (S O) d x) d H2 k t0 (lift (S O) (s k d) x0) H4) (lift (S O) d (THead k 
 x x0)) (lift_head k x x0 (S O) d))))) H3))))) H1))))))))) t1)).
+(* COMMENTS
+Initial nodes: 925
+END *)
 
 theorem subst1_lift_S:
  \forall (u: T).(\forall (i: nat).(\forall (h: nat).((le h i) \to (subst1 i 
@@ -161,4 +173,7 @@ h H1) k (lift (S h) (s k (S i)) t0) (lift (S h) (s k i) t0) (eq_ind_r nat (S
 (S h) (s k i) t0))) (H0 (s k i) h (le_trans h i (s k i) H1 (s_inc k i))) (s k 
 (S i)) (s_S k i))) (lift (S h) i (THead k t t0)) (lift_head k t t0 (S h) i)) 
 (lift (S h) (S i) (THead k t t0)) (lift_head k t t0 (S h) (S i))))))))))) u).
+(* COMMENTS
+Initial nodes: 1421
+END *)