proposition: Lemma setUb_alt f: fgraph f -> unionb f = union (range f).
proof: Proof. move=> fgf. set_extens t; first by move/setUb_P=> [y ty yx]; union_tac. move/setU_P => [z te]; move/(range_gP fgf) => [x xd eq]; union_tac; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)