proposition: Lemma tuto_in_cons : forall y s x, (x \in y :: s) = (x == y) || (x \in s).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)