update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / sn3 / lift1.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma b/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
index 1b64c22bb8bb500fd2a473021eefde1bc6959687..71d9e93fe566cef9074b090726d46fea7b999b88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/lift1.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sn3/props.ma".
+include "basic_1/sn3/props.ma".
 
-include "Basic-1/drop1/fwd.ma".
+include "basic_1/drop1/fwd.ma".
 
-include "Basic-1/lift1/fwd.ma".
+include "basic_1/lift1/props.ma".
 
-theorem sns3_lifts1:
+lemma sns3_lifts1:
  \forall (e: C).(\forall (hds: PList).(\forall (c: C).((drop1 hds c e) \to 
 (\forall (ts: TList).((sns3 e ts) \to (sns3 c (lifts1 hds ts)))))))
 \def
@@ -40,7 +40,4 @@ 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 *)