proposition: Lemma laws s: et_laws et s → ∀ vars: ∀ a, nat → carrier P a, eval_stmt et vars s.
proof: Proof. Proof with intuition. intros. generalize (@variety_laws et A _ _ _ s H1 (Pvars vars)). clear H1. destruct s as [x [? [t t0]]]. induction x as [| [x1 [t1 t2]]]; simpl in *; intros. unfold equiv, sig_equiv. rewrite (heq_eval_const vars t). rewrite (heq_eval_const vars t0)... apply IHx, H1. rewrite <- (heq_eval_const vars t1). rewrite <- (heq_eval_const vars t2)... Qed.
imports: Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra