proposition: Lemma foq_V r f b x: equivalence r -> lf_axiom f (substrate r) b -> inc x (quotient r) -> Vf (function_on_quotient r f b) x = f (rep x).
proof: Proof. by move => er ta xq; rewrite LfV //; apply: foq_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)