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