proposition: Lemma unionb_gr X : unionb (Lg (domain X) (Vg X)) = unionb X.
proof: Proof. set_extens t => /setUb_P; aw; move => [y ya yb]; apply/setUb_P; exists y => //. by move: yb;rewrite LgV. by aw. by rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)