proposition: Lemma familyP f : reflect (forall x, f x \in F x) (f \in family_mem (fmem F)).
proof: Proof. exact: forallP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)