stekoni fu'ivla

x1 is a list formed by head x2 and tail x3

Refers to the inductive definition of lists.