proposition: Lemma compose_fun_proj_ev2 r r' f x: equivalence r -> equivalence r' -> compatible_with_equivs (Lf f (substrate r) (substrate r')) r r' -> lf_axiom f (substrate r) (substrate r') -> inc x (substrate r) -> inc (f x) (substrate r') -> Vf (canon_proj r') (f x) = Vf (function_on_quotients r r' f \co canon_proj r) x.
proof: Proof. move=> er er' co ta xs fxs. have xsc: inc x (source (canon_proj r)) by aw. rewrite canon_proj_V // compfV //; last by apply: composable_fun_projs. set (y:= (Vf (canon_proj r) x)). have -> : (Vf (function_on_quotients r r' f) y = (Vf (fun_on_quotients r r' (Lf f (substrate r) (substrate r'))))y). have ys: inc y (quotient r) by rewrite /y canon_proj_V; fprops. have h :=(rep_i_sr er ys). rewrite foqs_V // foqcs_V //; aw; trivial; try apply: lf_function => //. by rewrite LfV. by rewrite - fun_on_quotient_pr5 // LfV // canon_proj_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)