proposition: Lemma tuto_mem_behead: forall s, {subset behead s <= s}.
proof: Proof. move=> [|y s] x //; exact: predU1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)