proposition: Lemma extension_partition_aux f x t h: partition_w_fam f x -> (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) -> (forall i j, inc i (domain f) -> inc j (domain f) -> agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)).
proof: Proof. move=> [fgf mdf ufx] afp. move=> i j id jd; case: (mdf _ _ id jd). move=> ->; rewrite setI2_id; move: (afp _ jd)=> [_ shj _]. hnf; rewrite shj; split;fprops => s //. rewrite/disjoint=> ->; hnf; split; try split; fprops. by move=> a /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)