X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst1%2Ffwd.ma;h=a2bc1edd668b06ca665594f20b0b7e656ee59a59;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=285a870e2c1ee6b9f0a8b14b28cd6191b40bdf00;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/fwd.ma
index 285a870e2..a2bc1edd6 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst1/fwd.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_gen_sort:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1 
@@ -27,6 +27,9 @@ i v (TSort n) x) \to (eq T x (TSort n))))))
 t (TSort n))) (refl_equal T (TSort n)) (\lambda (t2: T).(\lambda (H0: (subst0 
 i v (TSort n) t2)).(subst0_gen_sort v t2 i n H0 (eq T t2 (TSort n))))) x 
 H))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem subst1_gen_lref:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1 
@@ -44,6 +47,9 @@ nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2
 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i) 
 (eq T t2 (lift (S n) O v)) H1 H2)))) (subst0_gen_lref v t2 i n H0)))) x 
 H))))).
+(* COMMENTS
+Initial nodes: 305
+END *)
 
 theorem subst1_gen_head:
  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall 
@@ -104,6 +110,9 @@ T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 
 x1 H2 (subst1_single i v u1 x0 H3) (subst1_single (s k i) v t1 x1 H4))))))) 
 H1)) (subst0_gen_head k v u1 t1 t2 i H0)))) x H))))))).
+(* COMMENTS
+Initial nodes: 1199
+END *)
 
 theorem subst1_gen_lift_lt:
  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
@@ -127,6 +136,9 @@ x0))).(\lambda (H2: (subst0 i u t1 x0)).(ex_intro2 T (\lambda (t3: T).(eq T
 t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 t3)) x0 H1 
 (subst1_single i u t1 x0 H2))))) (subst0_gen_lift_lt u t1 t2 i h d H0)))) x 
 H))))))).
+(* COMMENTS
+Initial nodes: 395
+END *)
 
 theorem subst1_gen_lift_eq:
  \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall 
@@ -139,6 +151,9 @@ h))).(\lambda (H1: (subst1 i u (lift h d t) x)).(subst1_ind i u (lift h d t)
 (\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda 
 (t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t 
 u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
 
 theorem subst1_gen_lift_ge:
  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall 
@@ -161,4 +176,7 @@ x0))).(\lambda (H3: (subst0 (minus i h) u t1 x0)).(ex_intro2 T (\lambda (t3:
 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 (minus i h) u t1 t3)) x0 
 H2 (subst1_single (minus i h) u t1 x0 H3))))) (subst0_gen_lift_ge u t1 t2 i h 
 d H1 H0)))) x H)))))))).
+(* COMMENTS
+Initial nodes: 355
+END *)