proposition: Lemma sub_enumE : subenum =i P.
proof: Proof. move=> i. apply/idP/idP; rewrite !unfold_in. - by move=> /(allP subenumP). - by move=> /subenum_countE => H; apply/count_memPn; rewrite H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools