Plugins > Itauto

SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.