proposition: Lemma setUf2f x y f: unionf (doubleton x y) f = (f x) \cup (f y).
proof: Proof. set_extens t;last by case /setU2_P=> tf; union_tac. move/setUf_P => [z /set2_P []] -> h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)