proposition: Lemma foqs_V r r' f x: equivalence r -> equivalence r' -> lf_axiom f (substrate r)(substrate r') -> inc x (quotient r) -> Vf (function_on_quotients r r' f) x = class r' (f (rep x)).
proof: Proof. move => er er' ta xq. rewrite LfV//; last by apply: foqs_axioms. rewrite /fun_on_reps canon_proj_V //; apply: ta; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)