the Simplification of the Induction Conclusion (Step 4)

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

Click on the link above to apply the Axiom (CONSP (CONS x y)) = T.