Let $\Sigma$ denote an alphabet and $[ \Sigma ]$ set of lists over the alphabet.
I've encountered the following function:
$f([])=[]$
$f([x])=[x]$, for $x \in \Sigma$
$f(x:L)=f(L)$, for $x \in \Sigma$ and $L \in [ \Sigma ]$
The function is supposed to return a tail for nonempty list. That is:
$f([x_1,x_2,...,x_n])=[x_n]$
How would you understand the ":" operator in the definition?
Inductive proof should be possible for showing that this tail function is indeed working.
In this context, $:$ is the symbol that joins the head of a list to the rest of the list. Every list is either empty, or of the form $x : L$ for an element $x$ and a list $L$.
For example, the list $[1, 2, 3, 4]$ could be written $1 : 2 : 3 : 4 : []$. Let's see how your function $f$ acts on this. First, $1 : 2 : 3 : 4 : []$ is of the form $x : L$ with $x = 1$ and $L = 2 : 3 : 4 : []$. So by the definition of $f$, $f(1 : 2 : 3 : 4 : []) = f(x : L) = f(L) = f(2 : 3 : 4 : [])$. We can apply this again to get $f(3 : 4 : [])$ and then $f(4 : [])$. From there, since $4 : []$ is of the form $x : []$ (i.e. of the form $[x]$), the other part of the definition of $f$ applies: $f(4 : []) = [4]$.
So $f$ recursively cuts off the head of the list until just a single element remains. You can use induction on the length of the list (or structural induction if you know what that is) to prove that the function does what you think it does.