The right way of defining a predicate

Question

My theory contains a definition of lists: L(H,T) is a list, H is the first element (head), T is the list of remaining elements (tail), nil is empty list. So [A,B,C] = L(A,L(B,L(C,nil))). I defined equality for lists:

all X,Y : not(nil = L(X,Y)) ).
all Xh,Xt,Yh,Yt : (  L(Xh,Xt) = L(Yh,Yt)  <=>  ( Xh=Yh & Xt=Yt) ) ).

I also have a constant "c". I want to define a predicate TR(S,A,T), which should be true iff A is a list starting with "c":

all S,A,T,Tail : (  TR(S,A,T) <=> A=L(c,Tail) ).

But this axiom brings contradiction into my theory. What is the right way of defining TR?