X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr0%2Fsubst1.ma;h=877f87f0173178efff7dd6b792787dd45e958cf9;hb=b31c093c364e76cc6c4657008f3f259955311911;hp=0913488908021a7a7ec3189f636e7a2896378348;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/subst1.ma
index 091348890..877f87f01 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/subst1.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr0/props.ma".
+include "Basic-1/pr0/props.ma".
 
-include "LambdaDelta-1/subst1/defs.ma".
+include "Basic-1/subst1/defs.ma".
 
 theorem pr0_delta1:
  \forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (t1: T).(\forall 
@@ -29,6 +29,9 @@ T).(\lambda (t2: T).(\lambda (H0: (pr0 t1 t2)).(\lambda (w: T).(\lambda (H1:
 Abbr) u1 t1) (THead (Bind Abbr) u2 t))) (pr0_comp u1 u2 H t1 t2 H0 (Bind 
 Abbr)) (\lambda (t0: T).(\lambda (H2: (subst0 O u2 t2 t0)).(pr0_delta u1 u2 H 
 t1 t2 H0 t0 H2))) w H1)))))))).
+(* COMMENTS
+Initial nodes: 115
+END *)
 
 theorem pr0_subst1_back:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1 
@@ -47,6 +50,9 @@ T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t t0))) (\lambda (x: T).(\lambda
 (H2: (subst0 i u1 t1 x)).(\lambda (H3: (pr0 x t0)).(ex_intro2 T (\lambda (t: 
 T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t t0)) x (subst1_single i u1 t1 x 
 H2) H3)))) (pr0_subst0_back u2 t1 t0 i H0 u1 H1)))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 251
+END *)
 
 theorem pr0_subst1_fwd:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1 
@@ -65,6 +71,9 @@ T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t0 t))) (\lambda (x: T).(\lambda
 (H2: (subst0 i u1 t1 x)).(\lambda (H3: (pr0 t0 x)).(ex_intro2 T (\lambda (t: 
 T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t0 t)) x (subst1_single i u1 t1 x 
 H2) H3)))) (pr0_subst0_fwd u2 t1 t0 i H0 u1 H1)))))) t2 H))))).
+(* COMMENTS
+Initial nodes: 251
+END *)
 
 theorem pr0_subst1:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall 
@@ -90,4 +99,7 @@ w2)) (\lambda (w2: T).(subst1 i v2 t2 w2))) (\lambda (x: T).(\lambda (H4:
 (pr0 t0 x)).(\lambda (H5: (subst0 i v2 t2 x)).(ex_intro2 T (\lambda (w2: 
 T).(pr0 t0 w2)) (\lambda (w2: T).(subst1 i v2 t2 w2)) x H4 (subst1_single i 
 v2 t2 x H5))))) H3)) (pr0_subst0 t1 t2 H v1 t0 i H1 v2 H2)))))) w1 H0))))))).
+(* COMMENTS
+Initial nodes: 385
+END *)