X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr2%2Fsubst1.ma;h=47704dd52fb2c34deee41051808c212d30fae1c4;hb=8ae1653eb75d2b57c50e077c49cb9d078313ea9d;hp=35c106e6e9e498858285a6cf069fc26bd4dbb4a2;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/subst1.ma
index 35c106e6e..47704dd52 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr2/subst1.ma
@@ -14,19 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr2/defs.ma".
+include "Basic-1/pr2/defs.ma".
 
-include "LambdaDelta-1/pr0/subst1.ma".
+include "Basic-1/pr0/subst1.ma".
 
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
 
-include "LambdaDelta-1/csubst1/getl.ma".
+include "Basic-1/csubst1/getl.ma".
 
-include "LambdaDelta-1/csubst1/fwd.ma".
+include "Basic-1/csubst1/fwd.ma".
 
-include "LambdaDelta-1/subst1/subst1.ma".
+include "Basic-1/subst1/subst1.ma".
 
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
 
 theorem pr2_delta1:
  \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c 
@@ -39,6 +39,9 @@ T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t: T).(\lambda (H1: (subst1 i u t2
 t)).(subst1_ind i u t2 (\lambda (t0: T).(pr2 c t1 t0)) (pr2_free c t1 t2 H0) 
 (\lambda (t0: T).(\lambda (H2: (subst0 i u t2 t0)).(pr2_delta c d u i H t1 t2 
 H0 t0 H2))) t H1)))))))))).
+(* COMMENTS
+Initial nodes: 111
+END *)
 
 theorem pr2_subst1:
  \forall (c: C).(\forall (e: C).(\forall (v: T).(\forall (i: nat).((getl i c 
@@ -106,6 +109,9 @@ T).(subst1 i v t w2)) x0 (pr2_delta1 c e v i H19 w1 x H8 x0 H21) H20))))
 (subst1_confluence_eq t4 t v i (subst1_single i v t4 t H18) x H9))))))) 
 H14)))))))))) (pr0_subst1 t3 t4 H3 v w1 i H6 v (pr0_refl v))) c0 
 H5))))))))))))))) y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 1311
+END *)
 
 theorem pr2_gen_cabbr:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -269,4 +275,7 @@ O)))))))) (subst1_confluence_neq t4 t u i (subst1_single i u t4 t H2) (lift
 (S O) d0 x0) u0 d0 H11 (sym_not_eq nat d0 i (lt_neq d0 i H12)))))))))) 
 (pr0_gen_lift x1 x (S O) d0 H7))))) (pr0_subst1 t3 t4 H1 u0 (lift (S O) d0 
 x1) d0 H6 u0 (pr0_refl u0))))))))))))))))))))))) c t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 3757
+END *)