RonaldSK

Со списками обычно надо по индукции доказывать.
Theorem Dokaz1: forall A l1 l2, @PRIFIKS A l1 l2 -> exists l3, l2 = l1 ++ l3.
Proof.
intros.
induction H.
- exists l.
reflexivity.
- destruct IHPRIFIKS.
exists x0.
simpl.
rewrite H0.
reflexivity.
Qed.