proposition: Lemma extension_covering f t h (d:= domain f) (g := common_ext f h t) : (forall i, inc i d -> function_prop (h i) (Vg f i) t) -> (forall i j, inc i d -> inc j d -> agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)) -> [/\ function_prop g (unionb f) t, graph g = (unionb (Lg d (fun i => (graph (h i))))), Imf g = unionb (Lg d (fun i => (Imf (h i)))) & (forall i, inc i d -> agrees_on (Vg f i) g (h i))].
proof: Proof. move=> afp aag. have sg: (source g = unionb f) by rewrite /g /common_ext; aw. have tg: (target g = t) by rewrite /g/common_ext; aw. set u1:= unionb (Lg _ _). have gg: graph g = u1 by rewrite /u1/g/common_ext; aw. have gu: sgraph u1. move=> z /setUb_P; aw;move=> [y yd]; rewrite LgV // => zd. by move: (afp _ yd) => [ff _ _]; move: (function_sgraph ff); apply. have fgf: fgraph u1. rewrite /u1;split=>//. move => x y /setUb_P [u usf xghu] /setUb_P [v vsf yghv] sp. move: usf vsf; aw => usf vsf; move:xghu yghv. rewrite !LgV // => xghu yghv. move:(afp _ usf) (afp _ vsf) => [fu shu _] [fv shv _]. move: (Vf_pr2 fu xghu)(Vf_pr2 fv yghv) => qx qy. apply: pair_exten=>//. by apply: (function_sgraph fu). by apply: (function_sgraph fv). rewrite qx qy sp; apply: (proj33 (aag _ _ usf vsf)). by rewrite - shu - shv; apply: setI2_i ;[ rewrite - sp|]; Wtac. have fg: function g. rewrite /g/common_ext; apply: function_pr=>//. move=> z /funI_P [x /setUb_P];aw;move=> [y ysf]. rewrite LgV // => Jg ->. by move: (afp _ ysf)=> [fhy _ <-]; Wtac. set_extens z. move /setUb_P=> [y ysf zfy]; apply/(domainP gu); exists (Vf (h y) z). move: (afp _ ysf) => [fhy shy _]. apply /setUb_P; aw; ex_tac; bw => //; apply: Vf_pr3 => //; ue. move/(domainP gu) => [y]; move/setUb_P; aw;move=> [x xsf]; bw => // jg. move: (afp _ xsf) => [fhx shx _]; apply/setUb_P;ex_tac; rewrite - shx; Wtac. split => //. rewrite (ImfE fg) /g/common_ext; aw; set_extens zs. move/(rangeP gu)=> [x] /setUb_P; aw. move =>[y ysf]; rewrite LgV // => zfy. apply/setUb_P;move: (afp _ ysf) => [fhy shy _]; aw; ex_tac. rewrite LgV // (ImfE fhy); ex_tac. move/setUb_P; aw; move=> [y ysf]; bw => //. move: (afp _ ysf) => [fhy shy _];rewrite (ImfE fhy). move /(rangeP (function_sgraph fhy)) => [x Jg]. apply/(rangeP gu); exists x; apply/setUb_P; aw; ex_tac; rewrite LgV //. move=> y ysf; move: (afp _ ysf) => [fhy shy _]. split; first by rewrite sg; move=> x xfy; union_tac. by rewrite shy; fprops. move=> a afy /=; symmetry;apply: Vf_pr => //. rewrite gg; apply /setUb_P; aw; ex_tac; rewrite LgV //; Wtac; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)