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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/lift1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/lift1.ma
index a684670ba..1b64c22bb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/lift1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/lift1.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sn3/props.ma".
+include "Basic-1/sn3/props.ma".
 
-include "LambdaDelta-1/drop1/fwd.ma".
+include "Basic-1/drop1/fwd.ma".
 
-include "LambdaDelta-1/lift1/fwd.ma".
+include "Basic-1/lift1/fwd.ma".
 
 theorem sns3_lifts1:
  \forall (e: C).(\forall (hds: PList).(\forall (c: C).((drop1 hds c e) \to 
@@ -40,4 +40,7 @@ p) c e)).(\lambda (ts: TList).(\lambda (H1: (sns3 e ts)).(let H_x \def
 (H4: (drop1 p x e)).(eq_ind_r TList (lifts n n0 (lifts1 p ts)) (\lambda (t: 
 TList).(sns3 c t)) (sns3_lifts c x n n0 H3 (lifts1 p ts) (H x H4 ts H1)) 
 (lifts1 (PCons n n0 p) ts) (lifts1_cons n n0 p ts))))) H2))))))))))) hds)).
+(* COMMENTS
+Initial nodes: 323
+END *)