How come correctness proofs aren't tautological?
Membership is much more general than this recursive definition you give. At a higher level you could define membership as follows:

A tree can be defined as a collection of nodes, $V$, and edges $E$ where those edges and nodes satisfy particular constraints.
We say a value $x$ is a member of the tree if and only if there is a node $v$ in $V$ such that the value of $v$ is equivalent to $x$.

You then prove (probably with induction since it's recursive) that your function is equivalent to this definition. That is to say, your function returns true on value $x$ if and only if there is a node $v$ in $V$ such that the value of $v$ is equivalent to $x$.