proposition: Lemma pfamilyP (pT : predType rT) y D (F : aT -> pT) f : reflect (y.-support f \subset D /\ {in D, forall x, f x \in F x}) (f \in pfamily_mem y (mem D) (fmem F)).
proof: Proof. apply: (iffP familyP) => [/= f_pfam | [/supportP f_supp f_fam] x]. split=> [|x Ax]; last by have:= f_pfam x; rewrite Ax. by apply/subsetP=> x; case: ifP (f_pfam x) => //= _ fx0 /negP[]. by case: ifPn => Ax /=; rewrite inE /= (f_fam, f_supp). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)