ACL2-pc::elim
(atomic macro)
call the ACL2 theorem prover's elimination process
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!
