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