proposition: Lemma prefix_cons x s1 s2 : prefix (x :: s1) (x :: s2) <-> prefix s1 s2.
proof: Proof. by split=>E n; [apply: (E n.+1) | case: n]. 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)