(\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))).
(\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))).
(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)))))).
(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)))))).