proposition: Lemma foqc_V r f x: equivalence r -> function f -> source f = substrate r -> inc x (quotient r) -> Vf (fun_on_quotient r f) x = Vf f (rep x).
proof: Proof. move => er ff sf xq. rewrite compfV //. by rewrite section_canon_proj_V. by apply: foqc_axioms. by rewrite /section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)