The theorem prover's proof output is intended to suggest an outline
of the reasoning process employed by its proof engine, which is
virtually always more than is necessary for the ACL2 user. In
particular, the output often omits subgoals that are sufficiently
trivial, including tautologies.