proposition: Lemma eval_ext {V:Type0} (vs vs' : Vars V) : pointwise_paths@{Set U} vs vs' -> pointwise_paths@{Set U} (eval vs) (eval vs').
proof: Proof. intros E e;induction e;simpl;auto;apply ap011;auto. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra