proposition: Lemma setUb_identity x: unionb (identity_g x) = union x.
proof: Proof. rewrite /unionb identity_d setU_prop. by apply: setUf_exten => i ix /=; rewrite identity_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)