proposition: Lemma quotient_variety (et: EquationalTheory) `{InVariety et v} (e': ∀ s, relation (v s)) `{!Congruence et e'} (no_premises: ∀ s, et_laws et s → entailment_premises _ s ≡ nil): InVariety et v (e:=e').
proof: Proof. constructor. apply _. intros l law vars. pose proof (variety_laws l law vars) as E. pose proof (no_premises l law). destruct l as [prems [conc ?]]. simpl in *. subst. simpl in *. unfold equiv. rewrite E. pose proof (_: Equivalence (e' conc)). reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util