proposition: Lemma disjointU_P f x: inc x (disjointU f) <-> [/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
proof: Proof. split; first by apply: disjointU_hi. move => [pa pb pc]; apply/setUb_P; rewrite disjointU_d; ex_tac. rewrite LgV //; rewrite - {1} pc; apply/setXp_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)