Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) T)
Click on the link above to use the definition of IMPLIES
. Since the
conclusion of the implication is now identically T
, the implication
simplifies to T.