proposition: Lemma formula_substitution_eq env t xs : Forall (fun p => term_denote env (fst p) = term_denote env (snd p)) xs → formula_denote env (subst_all subst_formula t (substitutions xs)) = formula_denote env t.
proof: Proof. induction xs as [|[] ?]; simpl; intros; auto. inversion H. destruct (substitution t0 t1) eqn:?; intuition. destruct p; simpl. rewrite formula_denote_subst_formula; auto. now apply (term_denote_substitution Heqo). Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt