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!