proposition: Lemma extension_partition1 f x t h (g := common_ext f h t): partition_w_fam f x -> (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) -> (function_prop g x t /\ (forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
proof: Proof. move => pfa afp. move: (extension_covering afp (extension_partition_aux pfa afp)). by move: pfa => [fgf mdf ufx]; rewrite -/g - ufx; move => [h1 _ h2 h3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)