proposition: Lemma iim_fun_set1_i f x y: function f -> inc x (source f) -> y = Vf f x -> inc x (Vfi1 f y).
proof: Proof. move => ff xsf ->; apply /iim_fun_P; ex_tac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)