proposition: Lemma compose_fun_proj_eq r f b: equivalence r -> compatible_with_equiv (Lf f (substrate r) b) r -> lf_axiom f (substrate r) b -> (function_on_quotient r f b) \co (canon_proj r) = Lf f (substrate r) b.
proof: Proof. move=> er co ta. apply: function_exten; try solve [ rewrite/function_on_quotient; aw; trivial]. - apply: compf_f; apply: composable_fun_proj=>//. by apply: lf_function. - rewrite /function_on_quotient; aw =>x xs. by rewrite compose_fun_proj_ev // LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)