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