proposition: Lemma formula_size_subst_formula v v' m : formula_size (subst_formula m v v') = formula_size m.
proof: Proof. induction m; simpl; auto. now rewrite map_expr_size_subst_map_expr. Qed.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt