proposition: Lemma iim_fun_C1 f: function f -> {when eq^~ (target f) & sub^~ (target f), {morph Vfi f : a b / a -s b}}.
proof: Proof. move => ff a b -> btf. set_extens t. move/iim_fun_P=> [u /setC_P [utf ux] Jg];apply: setC_i. apply/iim_fun_P;ex_tac. by move/iim_fun_P=>[v vx Jvg]; case: ux;rewrite (Vf_pr ff Jg) -(Vf_pr ff Jvg). move/setC_P => [/iim_fun_P [u ut Jg] ne]; apply/iim_fun_P; ex_tac. apply/setC_i => //;dneg h; apply/iim_fun_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)