{V W:Type0 } (f : V -> W) (e : Expr V) : Expr W := match e with | Var v => Var (f v) | Zero => Zero | One => One | Plus a b => Plus ( f a) ( f b) | Mult a b => Mult ( f a) ( f b) | Neg a => Neg ( f a) end.
Require Import