Effective ATS:
Two Styles of Theorem-Proving in ATS