proposition: Lemma heq_eval vars {o} (t: T et o): heq (eval et vars t) (eval et (Pvars vars) t).
proof: Proof. Proof with intuition. induction t; simpl... unfold Pvars... simpl in IHt1. generalize (IHt1 (eval et vars t3)). clear IHt1. apply heq_proper. pose proof (@eval_proper et (carrier P) _ _ _ nat (ne_list.cons y t1)). apply H1; try intro... pose proof (@eval_proper et A _ _ _ nat (ne_list.cons y t1)). apply H1... unfold heq in IHt2. rewrite IHt2. apply (@eval_proper et A _ _ _ nat (ne_list.one y))... unfold impl, algebra_op. generalize (subset_closed P o). unfold algebra_op. generalize (AlgebraOps0 o). intros. induction (et o); simpl in *... 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