proposition: Lemma subenum_countE x : P x -> count_mem x subenum = 1.
proof: Proof. have:= subenumE x; rewrite !unfold_in => <-. by rewrite (count_uniq_mem _ subenum_uniq) unfold_in => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools