proposition: Lemma setUb_constant f x: constantgp f -> inc x (domain f) -> unionb f = Vg f x.
proof: Proof. move => p1 p2; set_extens t; last by move => p3; union_tac. by move /setUb_P => [y y1 y2]; rewrite (proj2 p1 _ _ p2 y1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)