X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr0%2Fsubst1.ma;h=05a93172a34796a6d5becc8c7844b0643bd67a01;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=877f87f0173178efff7dd6b792787dd45e958cf9;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/subst1.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/subst1.ma
index 877f87f01..05a93172a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr0/subst1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr0/subst1.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/pr0/props.ma".
+include "basic_1/pr0/subst0.ma".
 
-include "Basic-1/subst1/defs.ma".
+include "basic_1/subst1/fwd.ma".
 
-theorem pr0_delta1:
+lemma pr0_delta1:
  \forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (t1: T).(\forall 
 (t2: T).((pr0 t1 t2) \to (\forall (w: T).((subst1 O u2 t2 w) \to (pr0 (THead 
 (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w)))))))))
@@ -29,11 +29,8 @@ 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:
+lemma pr0_subst1_back:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1 
 i u2 t1 t2) \to (\forall (u1: T).((pr0 u1 u2) \to (ex2 T (\lambda (t: 
 T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t t2)))))))))
@@ -50,11 +47,8 @@ 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:
+lemma pr0_subst1_fwd:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst1 
 i u2 t1 t2) \to (\forall (u1: T).((pr0 u2 u1) \to (ex2 T (\lambda (t: 
 T).(subst1 i u1 t1 t)) (\lambda (t: T).(pr0 t2 t)))))))))
@@ -71,9 +65,6 @@ 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 
@@ -99,7 +90,4 @@ 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 *)