proposition: Lemma funI_set2 f a b: fun_image (doubleton a b) f = doubleton (f a) (f b).
proof: Proof. set_extens t; first by move/funI_P => [z] /set2_P;case => -> <-; fprops. move /set2_P; case => ->; apply: funI_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)