the Simplification of the Induction Conclusion (Step 7)
Subgoal *1/2'
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (IF T
(CONS (CAR A)
(APP (APP (CDR A) B)
C))
C)
(APP A (APP B C)))).
Click on the link above to apply the Axiom (IF T x y) = x.