proposition: Lemma cons_in_map_cons a b s w (l : seq (seq T)) : a :: s \in [seq b :: s1 | s1 <- l] -> a == b.
proof: Proof. Proof using. elim: l => // l0 l IHl; rewrite map_cons in_cons => /orP[]; last exact: IHl. by move=> /eqP[->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)