proposition: Lemma pffun_onP y D R f : reflect (y.-support f \subset D /\ {subset image f D <= R}) (f \in pffun_on_mem y (mem D) (mem R)).
proof: Proof. apply: (iffP (pfamilyP y D (fun _ => R) f)) => [] [-> f_fam]; split=> //. by move=> _ /imageP[x Ax ->]; apply: f_fam. by move=> x Ax; apply: f_fam; apply/imageP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)