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.
