How come correctness proofs aren’t tautological?

Consider the following function on binary trees, which is supposed to tell whether a given int is a member of a binary tree t:

type tree = Leaf | Node of int * tree * tree;;  let rec tmember (t:tree) (x:int) : bool =   match t with       Leaf -> false     | Node (j,left,right) -> j = x || tmember left x || tmember right x ;; 

If one wants to prove that this function is correct, one would need to define first what tree membership actually means, but then I can find no formal way of doing this except for saying that x is a member of t if and only if it is either equal to the root of t, or it is a member of the left or right subtree of t. This is essentially saying that x is a member of t if and only if tmember t x outputs true.

What am I missing here?