proposition: Lemma compose_fun_proj_ev r f b x: equivalence r -> compatible_with_equiv (Lf f (substrate r) b) r -> inc x (substrate r) -> lf_axiom f (substrate r) b -> Vf (function_on_quotient r f b \co canon_proj r) x = f x.
proof: Proof. move=> er co xr ta. have cq: (inc (class r x) (quotient r)) by fprops. have cop:= composable_fun_proj er ta. have rrx: related r (rep (class r x)) x. by apply: symmetricity_e=>//; apply: related_rep_class=>//. rewrite compfV // ? canon_proj_s // canon_proj_V // foq_V //. move: (proj33 co _ _ rrx); rewrite ! LfV //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)