proposition: Lemma prefix_cons' x y s1 s2 : prefix (x :: s1) (y :: s2) -> x = y /\ prefix s1 s2.
proof: Proof. by move=>H; case: (H 0 x (erefl _)) (H)=>-> /prefix_cons. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)