proposition: Lemma cover_at_pr f x y i: partition_w_fam f x -> inc i (domain f) -> inc y (Vg f i) -> cover_at f y = i.
proof: Proof. move => h idf yv. have [fgf md uf] := h. have zx: inc y x by rewrite -uf; union_tac. have [yfc cd]:= (cover_at_in h zx). case: (md _ _ cd idf) => // di; empty_tac1 y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)