(u : Symbol σ) : ComputeOpQuotient u.#A u.#QuotientAlgebra. Proof. apply op_quotient_algebra. Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.