(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/drop1/defs.ma".
+include "Basic-1/drop1/defs.ma".
theorem drop1_gen_pnil:
\forall (c1: C).(\forall (c2: C).((drop1 PNil c1 c2) \to (eq C c1 c2)))
(\lambda (_: PList).Prop) with [PNil \Rightarrow False | (PCons _ _ _)
\Rightarrow True])) I PNil H4) in (False_ind (eq C c3 c5) H5)))))))))))) y c1
c2 H0))) H))).
+(* COMMENTS
+Initial nodes: 198
+END *)
theorem drop1_gen_pcons:
\forall (c1: C).(\forall (c3: C).(\forall (hds: PList).(\forall (h:
(n: nat).(drop n d c2 c4)) H12 h H9) in (ex_intro2 C (\lambda (c6: C).(drop h
d c2 c6)) (\lambda (c6: C).(drop1 hds c6 c5)) c4 H13 H11)))))))) H6))
H5)))))))))))) y c1 c3 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 587
+END *)