proposition: Lemma cons2_infix s1 s2 x : infix (x :: s1) (x :: s2) -> infix s1 s2.
proof: Proof. by rewrite /= eqxx /= -cat1s => /orP[/prefixW//|]; exact: catl_infix. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)