proposition: Lemma up_inter2 x y: intersectionU2 U inc' x y = g (f x \cap f y).
proof: Proof. move:up_values => [pa pb pc pd [pe pf]]. rewrite /intersectionU2 pd. apply: f_equal. set_extens t; first by move /Zo_P => /setI2_P. by move /setI2_P => h; apply/Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)