Type := ∀ (u : Symbol σ), ClosedUnderOp u.#A. Global Instance trunc_is_closed_under_ops {n} `{∀ s x, IsTrunc n (P s x)} : IsTrunc n . Proof. apply istrunc_forall. Qed.
Require Import Import algebra_notations ne_list.notations. Import subalgebra_notations.