proposition: Lemma setIf2f x y f: intersectionf (doubleton x y) f = (f x) \cap (f y).
proof: Proof. have ned:= (set2_ne x y). set_extens z. move /(setIf_P _ ned) => h; apply setI2_i; apply: h; fprops. by move/setI2_P => [zx zy]; apply: (setIf_i ned) => j; case/set2_P => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)