proposition: Lemma formula_sound env t : (if formula_tauto env t then True else False) → formula_denote env t.
proof: Proof. unfold formula_tauto; destruct t, (formula_backward _ env); tauto. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt