proposition: Theorem extension_partition_thm f x t h: partition_w_fam f x -> (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) -> exists! g, (function_prop g x t /\ (forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
proof: Proof. move => pfa afp. have aah:= (extension_partition_aux pfa afp). move: pfa => [fgf mdf <-]; exact: (extension_covering_thm afp aah fgf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)