proposition: Lemma setUb_rewrite f g: fgraph f -> range f = domain g -> unionb g = unionb (g \cf f).
proof: Proof. rewrite /composef=> fgf rfsg. set_extens t; move/setUb_P => [a pa pb]; apply/setUb_P. move: pa; rewrite- rfsg; move /(range_gP fgf) => [x xd etc]. aw; ex_tac; rewrite LgV //; ue. move: pa;aw => pa. move: pb; rewrite LgV // - rfsg => ta; exists (Vg f a); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)