fact: Fixpoint expr_map {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 (expr_map f a) (expr_map f b) | Mult a b => Mult (expr_map f a) (expr_map f b) | Neg a => Neg (expr_map f a) end.
imports: HoTT.Classes.interfaces.abstract_algebra