fact: Fixpoint prefix s1 s2 {struct s2} := if s1 isn't x :: s1' then true else if s2 isn't y :: s2' then false else (x == y) && prefix s1' s2'.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)