Proof_search
Refl_tauto
G_rtauto