Prefix encoding of algebraic data types
A code is prefix-free if there does not exist any distinct two values v, w such that encode(v) is a prefix of encode(w).  So, to prove that your encoding is prefix-free, you start by considering two arbitrary distinct values v, w and demonstrate that encode(v) is not a prefix of encode(w).

I suggest you use proof by induction on the "size" of the largest value, so you'll consider two arbitrary values v, w that are both of size at most $n$.  In this case, a reasonable choice for the "size" is the number of times the recursion was applied, i.e., the number of cells in the list.  Your inductive predicate $P(n)$ states that for every pair of distinct values v, w both of whose size is at most $n$, encode(v) is not a prefix of encode(w).  You want to prove $P(n)$ for all $n$.  To do that using the principle of induction, you need to prove $P(0)$ and prove $P(n) \implies P(n+1)$.  Here $P(0)$ is trivial, so we can focus on the inductive step $P(n) \implies P(n+1)$.

For your example of the list data structure, that shouldn't be too hard.  You'll just case-split on the size and structure of v, w.  There are four cases:


case (a): v has size $\le n$, w has size $\le n$
case (b): v has size $\le n$, w has size $n+1$
case (c): v has size $n+1$, w has size $\le n$
case (d): v has size $n+1$, w has size $n+1$


Case (a) is already covered by $P(n)$, so you only need to reason about the three other cases.  Each one can be handled by using the induction predicate.

I'll describe how to prove case (d).  You should be able to see how to handle the other cases similarly.  Let a = hd(v) and k = tl(v), so that v == a::k.  Similarly let b = hd(w) and l = tl(w) so that w == b::l.  We can see that

encode(v) == encode(1) &lt;&gt; encode(a) &lt;&gt; encode(k)
encode(w) == encode(1) &lt;&gt; encode(b) &lt;&gt; encode(l)


Now we assumed that v, w are distinct, i.e., v != w.  It follows that either a != b or k != l.  If a != b, the fact that encode is prefix-free on ground terms implies that encode(a) is not a prefix of encode(b), which in turn implies that encode(v) is not a prefix of encode(w).  If a == b and k != l, the inductive hypothesis $P(n)$ implies that encode(k) is not a prefix of encode(l) (since both k and l have size one less than v, w, i.e., size $n$), which in turn implies that encode(v) is not a prefix of encode(w).

Ultimately, once you've handled all four cases, you'll have proven that encode(v) is not a prefix of encode(w) for an arbitrary pair of distinct values v, w of size $n+1$, from which $P(n+1)$ follows.

The same techniques can be applied to any algebraic data types that is formed as a recursive combination of products and co-products.