fact: Fixpoint formula_size (t : formula) : nat := match t with | Top => 1%nat | Bottom => 1%nat | Maps _ _ _ m => 1%nat + map_expr_size m | Impl p q => 1%nat + formula_size p + formula_size q end.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt