Induction on a is unflawed: every occurrence of a in the conjecture
(equal (app (app a b) c) (app a (app b c)))is in a position being recursively decomposed!
Now look at the occurrences of
b. The first (shown in bold below)
is in a position that is held constant in the recursion of
(app a b).
It would be ``bad'' to induct on
(equal (app (app a b) c) (app a (app b c)))