fact: Fixpoint formula_denote env (t : formula) : Prop := match t with | Top => True | Bottom => False | Maps x y f m => M.MapsTo (term_denote env x, term_denote env y) (term_denote env f) (map_expr_denote env m) | Impl p q => formula_denote env p → formula_denote env q end.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt