ACL2-PC::ELIM

(atomic macro) call the ACL2 theorem prover's elimination process
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
elim

Upon running the elim command, the system will create a subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof, where only elimination is used; not even simplification is used!