proposition: Lemma iim_fun_set1_P f y: function f -> forall x, inc x (Vfi1 f y) <-> (inc x (source f) /\ y = Vf f x).
proof: Proof. move => ff x; split. move /iim_fun_P => [u /set1_P -> pa]; split;Wtac. by move => [pa pb]; apply:iim_fun_set1_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)