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