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