proposition: Lemma laws_hold s (L: et_laws et s): ∀ vars, eval_stmt _ vars s.
proof: Proof. Proof with simpl in *; intuition. intros. rewrite boring_eval_entailment. destruct s. simpl in *. intros. apply (e_law _ L vars). clear L. induction entailment_premises... subst... Qed.
imports: Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms MathClasses.interfaces.universal_algebra MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.categories.varieties