{w : SymbolType σ} : ∀ (α : Operation A w), ClosedUnderOp A P α → Operation carriers_subalgebra w := match w with | [:t:] => λ α c, (α; c) | s ::: w' => λ α c x, (α x.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.