Induction on binary trees
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 Binary Trees: To prove
Base Case: (implies (atom x) (p x))
Induction Step: (implies (and (not (atom x)) (p (car x)) (p (cdr x))) (p x))
An argument analogous to that given in example-induction-scheme-on-lists should convince you that
A function that suggests this induction is: