proposition: Lemma partial_fun1_axioms x: lf_axiom (fun y=> Vf f (J x y))(im_of_singleton (source f) x) (target f).
proof: Proof. move=> t /dirim_P [u /set1_P ->]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)