Induction on several variables
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.
Induction on Several Variables To
Base Case 1: (implies (endp x) (p n x))
Base Case 2: (implies (and (not (endp x)) (zp n)) (p n x))
Induction Step: (implies (and (not (endp x)) (not (zp n)) (p (- n 1) (cdr x))) (p n x))
A function that suggests this induction is