proposition: Lemma foq_f r f b: equivalence r -> lf_axiom f (substrate r) b -> function (function_on_quotient r f b).
proof: Proof. by rewrite /function_on_quotient=> *; apply: lf_function; apply: foq_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)