proposition: Lemma setUb_rewrite1 f g: function f -> fgraph g -> Imf f = domain g -> unionb g = unionb (g \cf (graph f)).
proof: Proof. move => ff; rewrite (ImfE ff) => fgg; apply: setUb_rewrite. by case:ff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)