proposition: Lemma formula_size_subst_all_formula defs m : formula_size (subst_all subst_formula m defs) = formula_size m.
proof: Proof. induction defs; simpl; auto. destruct a. now rewrite formula_size_subst_formula. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt