(* 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
(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 *)