proposition: Lemma laws_hold s: et_laws et s → ∀ vars, eval_stmt et vars s.
proof: Proof. intros. pose proof (λ i, variety_laws s H2 (λ sort n, vars sort n i)). clear H2. assert (∀ i : I, eval_stmt (et_sig et) (λ (sort : sorts (et_sig et)) (n : nat), vars sort n i) (entailment_as_conjunctive_statement (et_sig et) s)). intros. rewrite <- boring_eval_entailment. apply (H3 i). clear H3. rewrite boring_eval_entailment. destruct s. simpl in *. destruct entailment_conclusion. simpl in *. destruct i. simpl in *. intro. apply component_equality_to_product with (λ i, eval et (λ sort n, vars sort n i) t) (λ i, eval et (λ sort n, vars sort n i) t0). intro. apply H2. clear H2. simpl. induction entailment_premises... simpl in *. intuition. simpl. rewrite <- (nqe_always (fst (projT2 a)) vars i). rewrite <- (nqe_always (snd (projT2 a)) vars i). intuition. apply H3. apply IHentailment_premises. apply H3. apply nqe_always. apply nqe_always. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories MathClasses.categories.varieties