proposition: Lemma foqs_axioms r r' f: equivalence r -> equivalence r' -> lf_axiom f (substrate r)(substrate r') -> lf_axiom (fun_on_reps r' f) (quotient r) (quotient r').
proof: Proof. move => er er' h x xs. have w: (inc (rep x) (substrate r)) by fprops. rewrite /fun_on_reps canon_proj_V //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)