proposition: Lemma prefixP (A : eqType) (s1 s2 : seq A) : reflect (prefix s1 s2) (seq.prefix s1 s2).
proof: Proof. apply/(equivP (seq.prefixP (s1:=s1) (s2:=s2))). by apply: iff_sym; exact: prefixE. 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)