proposition: Lemma extension_covering_thm f t h (d:= domain f): (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)) -> fgraph f -> exists! g, (function_prop g (unionb f) t /\ (forall i, inc i d -> agrees_on (Vg f i) g (h i))).
proof: Proof. move=> afp aag fgf; apply /unique_existence;split. move: (extension_covering afp aag)=> [p1 p2 p3 p4]. by exists (common_ext f h t). rewrite /function_prop=> x y [[fx sx tx] agx] [[fy sy ty] agy]. apply: function_exten=>//; try ue. have c: (covering f (unionb f)) by split => //. suff agi: (forall i, inc i d -> agrees_on ((unionb f) \cap (Vg f i)) x y). move:(proj33 (agrees_on_covering c fx fy sx sy agi)); rewrite sx;apply. move=> i isf; hnf. split;first by rewrite sx;apply: subsetI2l. by rewrite sy;apply: subsetI2l. move => a /setI2_P; move: (proj33 (agx _ isf)) (proj33 (agy _ isf)). rewrite /agrees_on; move=> p1 p2 [_ afi]. by rewrite (p1 _ afi) (p2 _ afi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)