Subsumption of Induction Candidates in App Example
After collecting induction suggestions from these three terms
(app a b) (app b c) (app a (app b c))
the system notices that the first and last suggest the same decomposition
Decompose a as we would to unwind (app a b).
Decompose b as we would to unwind (app b c).