proposition: Lemma lf_recovers f: function f -> Lf (Vf f)(source f)(target f) = f.
proof: Proof. move=> ff. have ta: (lf_axiom (Vf f) (source f) (target f)) by move=> x /=; fprops. apply: function_exten; aw=> //; [ by apply: lf_function | by move => x xf; bw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)