After collecting induction suggestions from these three terms
(app a b)the system notices that the first and last suggest the same decomposition of
(app b c)
(app a (app b c))
a. So we are left with two ideas about how to induct:
Decompose a as we would to unwind (app a b).
Decompose b as we would to unwind (app b c).