{w : SymbolType σ} (g : Operation (A/Φ) w) (α : Operation A w) (β : Operation B w) (G : ComputeOpQuotient A Φ α g) (P : OpPreserving f α β) : OpPreserving def_hom_quotient_algebra_mapout g β. Proof. unfold ComputeOpQuotient in G. induction w; cbn in *. - destruct (G tt)^. apply P. - refine (Quotient_ind_hprop (Φ t) _ _). intro x. apply (IHw (g (class_of (Φ t) x)) (α x) (β (f t x))). + intro a. apply (G (x,a)). + apply P. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.