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: case split on whether a is empty (i.e., (endp a)), and in the case where it is not empty, recursively process (cdr 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).