IsClosedUnderOps (A/Φ) is_subalgebra_class. Proof. intro u. eapply op_closed_subalgebra_is_subalgebra_class. - apply compute_op_quotient. - apply is_closed_under_ops_subalgebra_predicate. exact _. Qed.
Require Import Import