### 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!