proposition: Lemma lf_function f a b: lf_axiom f a b -> function (Lf f a b).
proof: Proof. move=> ta; apply: function_pr; aw; fprops. by move=> t; rewrite Lg_range; move/funI_P=> [z zb ->]; apply: ta. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)