proposition: Theorem extension_psetX f J g: nonempty_fam f -> fgraph g -> domain g = J -> sub J (domain f) -> (forall i, inc i J -> inc (Vg g i) (Vg f i)) -> exists h, [/\ domain h = domain f, fgraph h, (forall i, inc i (domain f) -> inc (Vg h i) (Vg f i)) & {inc J, h =1g g} ].
proof: Proof. move=> alne fg dg sjdf iVV. set (h:= g \cup (unionf ((domain f) -s J) (fun i => (singleton (kpair i (rep (Vg f i))))))). have hg: sgraph h. move=>t;case /setU2_P; first by move: fg=> [gg _]; apply: gg. move/setUf_P=> [y _ /set1_P ->]; fprops. have dh: domain h = domain f. set_extens t. move /(domainP hg) => [y /setU2_P []]. move=> Jg; apply: sjdf; rewrite -dg; aw; fprops; ex_tac. move /setUf_P => [y' yc /set1_P Js]. by rewrite (pr1_def Js); move /setC_P: yc => []. move => tdf; apply/(domainP hg);case: (inc_or_not t J). by rewrite -dg; move/(domainP (proj1 fg)) => [y jg];exists y; apply:setU2_1. move=> ntj; exists (rep (Vg f t)). apply:setU2_2; apply /setUf_P; exists t;fprops. have fgh: fgraph h. split =>//. move => x y; case /setU2_P => x1; case /setU2_P => y1. - by move: fg=> [_ ]; apply. - move/setUf_P: y1 => [z /setC_P [_ nzj] /set1_P eq1] eq2. move: (domain_i1 x1); rewrite dg eq2 eq1; aw; contradiction. - move/setUf_P: x1 => [z/setC_P [_ nzj] /set1_P eq1] eq2. move: (domain_i1 y1); rewrite dg - eq2 eq1; aw; contradiction. - move/setUf_P: x1 => [x1 _ /set1_P ->]; aw. by move/setUf_P: y1 => [y1 _ /set1_P ->]; aw => ->. have sV: forall i, inc i J -> Vg h i = Vg g i. have sgh: (sub g h) by move=> t; rewrite /h; aw; fprops. by move=> i; rewrite -dg=> ij; symmetry; apply: (sub_graph_ev fgh sgh ij). exists h; split => // i id. case: (inc_or_not i J)=> hyp; first by rewrite sV //; apply: iVV. have ic: (inc i ((domain f) -s J)) by fprops. have Jh: (inc (kpair i (rep (Vg f i))) h). by rewrite /h; apply: setU2_2; union_tac. by move: (pr2_V fgh Jh); aw; move=> <-; apply: rep_i; apply: alne. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)