"formula_equality" theory