proposition: Lemma inverse_direct_image_inj f x: injection f -> sub x (source f) -> Vfs (inverse_fun f) (Vfs f x) = x.
proof: Proof. move=> [ff fi] xsf. apply: extensionality; last by apply: inverse_direct_image. rewrite -iim_fun_pr => y /iim_graph_P [u ui Jg]. move /(Vf_image_P ff xsf): ui => [v vx]; rewrite (Vf_pr ff Jg) => Vv. by rewrite - (fi _ _ (xsf _ vx) (p1graph_source ff Jg) (sym_eq Vv)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)