proposition: Lemma disjointU_pi f x y: inc y (domain f) -> inc x (Vg f y) -> inc (J x y) (disjointU f).
proof: Proof. move => ta tb;apply/disjointU_P; aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)