{w : SymbolType σ} : QuotOp w. Proof. refine ( match w return QuotOp w with | [:s:] => λ (f : A s) P, (class_of (Φ s) f; λ a, idpath) | s ::: w' => λ (f : A s → Operation A w') P, (Quotient_rec (Φ s) _ (λ (x : A s), op_qalg_cons f P x) (op_quotient_algebra_well_def s w' f P) ; _) end ). intros [x a]. apply ( w' (f x) (op_compatible_cons Φ s w' f x P)). Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.