proposition: Lemma foq_finer_V x: finer_equivalence s r -> inc x (quotient s) -> Vf (fun_on_quotient s (canon_proj r)) x = class r (rep x).
proof: Proof. move: fa => [es er fh] fe xq. rewrite foqc_V // ?canon_proj_V // ? fh; aw; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)