Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
Start in a fresh ACL2, either by restarting your ACL2 image from scratch or
executing :ubt! 1.
Use The Method to prove
(defthm subsetp-reflexive (subsetp x x))
When you've solved this problem, compare your answer to ours; see introductory-challenge-problem-2-answer.
Then, use your browser's Back Button to return to introductory-challenges.
