proposition: Lemma prefix_cons' x y s1 s2 : prefix (x :: s1) (y :: s2) -> x = y /\ prefix s1 s2.
proof: Proof. move=>H; move: (H 0 x (erefl _))=>[H']. by move: H; rewrite H' prefix_cons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq)