the Simplification of the Induction Conclusion (Step 9)

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C))))
         (EQUAL (CONS (CAR A)
                      (APP (APP (CDR A) B)
                           C))
                (CONS (CAR A)
                      (APP (CDR A) (APP B C))))).

Click on the link above to apply the Axiom that (EQUAL (CONS x y) (CONS u v)) is equal to the conjunction of (EQUAL x u) and (EQUAL y v). In this case, (EQUAL x u) is trivial, (EQUAL (CAR A) (CAR A)).