proposition: Lemma extension_partition2 f x t h (g:= common_ext f (fun i => (triple (Vg f i) t (graph (h i)))) t): partition_w_fam f x -> (forall i, inc i (domain f) -> function_prop_sub (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=> pf prop. pose nh i := triple (Vg f i) t (graph (h i)). have afp: forall i, inc i (domain f) -> function_prop (nh i) (Vg f i) t. move=> i id; move: (prop _ id) => [fgh sg th];rewrite /nh. saw; apply: function_pr; fprops. by apply: sub_trans th; apply: f_range_graph. by rewrite domain_fg. have [fpg aag] := (extension_partition1 pf afp). split=>// => i idf; move: (aag _ idf)=> [aa cc bb];split=>//. by move: (prop _ idf) => [_ -> _]; fprops. by move=> a aV; rewrite /g /nh (bb _ aV) /nh /Vf; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)