proposition: Lemma formula_denote_subst_formula env v v' t : term_denote env v = term_denote env v' → formula_denote env (subst_formula t v v') = formula_denote env t.
proof: Proof. induction t; simpl; auto; intros. - rewrite map_expr_denote_subst_map_expr, !term_denote_subst_term; auto. - rewrite IHt1, IHt2; auto. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt