fact: Fixpoint map_expr_denote env (m : map_expr) : M.t N := match m with | Empty => M.empty N | Add x y f m' => M.add (term_denote env x, term_denote env y) (term_denote env f) (map_expr_denote env m') end.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt