proposition: Lemma tuto_mem_cat : forall x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
proof: Proof. by move=> x s1 s2; elim: s1 => //= y s1 IHs; rewrite !inE /= -orbA -IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)