X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst0%2Ffwd.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst0%2Ffwd.ma;h=165555fe2fed927839b9c759928eb01a56c48076;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=4b387483e16e9e23b29af037f9440f983b9f2842;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/fwd.ma
index 4b387483e..165555fe2 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst0/defs.ma".
+include "Basic-1/subst0/defs.ma".
 
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
 
 theorem subst0_gen_sort:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0 
@@ -52,6 +52,9 @@ u1 t1) (TSort n))).(let H6 \def (eq_ind T (THead k u1 t1) (\lambda (ee:
 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
 (TSort n) H5) in (False_ind P H6)))))))))))))) i v y x H0))) H)))))).
+(* COMMENTS
+Initial nodes: 445
+END *)
 
 theorem subst0_gen_lref:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0 
@@ -96,6 +99,9 @@ n)) \to (land (eq nat n (s k i0)) (eq T t2 (lift (S n) O v0)))))).(\lambda
 \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
 True])) I (TLRef n) H5) in (False_ind (land (eq nat n i0) (eq T (THead k u2 
 t2) (lift (S n) O v0))) H6)))))))))))))) i v y x H0))) H))))).
+(* COMMENTS
+Initial nodes: 779
+END *)
 
 theorem subst0_gen_head:
  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall 
@@ -297,6 +303,9 @@ T).(subst0 (s k i0) v0 t1 t3)))) (ex3_2_intro T T (\lambda (u3: T).(\lambda
 (_: T).(subst0 i0 v0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k 
 i0) v0 t1 t3))) u2 t2 (refl_equal T (THead k u2 t2)) H16 H14)))) k0 
 H10)))))))) H7)) H6)))))))))))))) i v y x H0))) H))))))).
+(* COMMENTS
+Initial nodes: 4255
+END *)
 
 theorem subst0_gen_lift_lt:
  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
@@ -480,6 +489,9 @@ t x3 i H12 k t0 x2 H10)) (THead k (lift h (S (plus i d)) x3) (lift h (s k (S
 i h d H5))))) (H0 x1 (s k i) h d H8)))) x H4)))))) H3)) (subst0_gen_head k 
 (lift h d u) (lift h (S (plus i d)) t) (lift h (s k (S (plus i d))) t0) x i 
 H2))))))))))))) t1)).
+(* COMMENTS
+Initial nodes: 5157
+END *)
 
 theorem subst0_gen_lift_false:
  \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall 
@@ -551,6 +563,9 @@ T).(\lambda (t2: T).(subst0 (s k i) u (lift h (s k d) t1) t2))) P (\lambda
 (subst0 i u (lift h d t0) x0)).(\lambda (_: (subst0 (s k i) u (lift h (s k d) 
 t1) x1)).(H u x0 h d i H1 H2 H7 P)))))) H5)) (subst0_gen_head k u (lift h d 
 t0) (lift h (s k d) t1) x i H4))))))))))))))))) t).
+(* COMMENTS
+Initial nodes: 1621
+END *)
 
 theorem subst0_gen_lift_ge:
  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
@@ -707,4 +722,7 @@ x1 H8) x0 H10)))) (H x0 i h d H6 H2))))) (H0 x1 (s k i) h (s k d) H7 (eq_ind
 nat (s k (plus d h)) (\lambda (n: nat).(le n (s k i))) (s_le k (plus d h) i 
 H2) (plus (s k d) h) (s_plus k d h)))) x H5)))))) H4)) (subst0_gen_head k u 
 (lift h d t) (lift h (s k d) t0) x i H3)))))))))))))) t1)).
+(* COMMENTS
+Initial nodes: 4191
+END *)