proposition: Lemma cover_at_in f x y (i := cover_at f y): partition_w_fam f x -> inc y x -> (inc y (Vg f i) /\ inc i (domain f)).
proof: Proof. move=> [fg md ufx] yx; apply: select_pr. by move: yx; rewrite - ufx; move/setUb_P. move=> k j id yif jd yjf. have yi: (inc y ((Vg f k) \cap (Vg f j))) by fprops. case: (md k j id jd) =>// di;empty_tac1 y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)