proposition: Lemma map_expr_denote_subst_map_expr env v v' m : term_denote env v = term_denote env v' → map_expr_denote env (subst_map_expr m v v') = map_expr_denote env m.
proof: Proof. induction m; simpl; auto; intros. rewrite IHm; auto. now rewrite !term_denote_subst_term. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt