Induction on lists
See logic-knowledge-taken-for-granted-inductive-proof for an explanation of what we mean by the induction suggested by a recursive function or a term.
Classical Induction on Lists: To prove
Base Case: (implies (endp x) (p x))
Induction Step: (implies (and (not (endp x)) (p (cdr x))) (p x))
An argument analogous to that given for natural numbers, example-induction-scheme-nat-recursion, establishes
A function that suggests this induction is
(defun app (x y) (if (endp x) y (cons (car x) (app (cdr x) y)))).