proposition: Lemma injective_pr_bis f: function f -> (forall y, singl_val (fun x => related (graph f) x y)) -> injection f.
proof: Proof. move=> ff prop;split => // x y xs ys Weq; apply: (prop (Vf f x) x y). by apply: (Vf_pr3 ff xs). by rewrite Weq; apply: (Vf_pr3 ff ys). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)