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.