{w : SymbolType σ} (γ : Operation (A/Φ) w) (α : Operation A w) (Q : ComputeOpQuotient A Φ α γ) (C : ClosedUnderOp A P α) : ClosedUnderOp (A/Φ) is_subalgebra_class γ. Proof. induction w. - specialize (Q tt). apply tr. exists (α; C). cbn in Q. destruct Q^. exact (EquivRel_Reflexive α). - refine (Quotient_ind_hprop (Φ t) _ _). intro x. refine (Trunc_rec _). intros [y R]. apply (IHw (γ (class_of (Φ t) x)) (α (i t y))). + intro a. destruct (qglue R)^. apply (Q (i t y,a)). + apply C. exact y.2. Qed.
Require Import Import