fact: Definition holds {σ: signature} {V: varspec σ} (a: algebra σ) (e: equation σ V) : UU := ∏ α, fromterm (ops a) α (eqsort e) (lhs e) = fromterm (ops a) α (eqsort e) (rhs e).
imports: UniMath.MoreFoundations.Notations UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.Equations