proposition: Lemma foq_axioms r f b: equivalence r -> lf_axiom f (substrate r) b -> lf_axiom (fun_on_rep f) (quotient r) b.
proof: Proof. move=> er h x xs;apply: h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)