proposition: Lemma setUb_P1 x a f: inc x (unionb (Lg a f)) <-> exists2 y, inc y a & inc x (f y).
proof: Proof. split. move /setUb_P; aw => - [y ya]; rewrite (LgV ya) => yf; ex_tac. by move => [y ya xf]; apply /setUb_P; aw; ex_tac; bw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)