fact: Fixpoint eval {V} {n: OpType} (vars: Vars A V) (t: Term V n) {struct t}: op_type A n := match t with | Var v a => vars a v | Op _ o => algebra_op o | App _ n a f p => eval vars f (eval vars p) end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic