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 of 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).