fact: Record EquationalTheory := { et_sig:> Signature ; et_laws:> EqEntailment et_sig → Prop }.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic