{w : SymbolType σ} (α : Operation A w) (C : ClosedUnderOp A P α) : OpPreserving def_inc_subalgebra (op_subalgebra A P α C) α. Proof. induction w. - reflexivity. - intros x. apply IHw. Defined.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.