let rec
   append = lambda a. lambda b.
      if null a then b else (hd a)::(append tl a b),

   ListEq = lambda x. lambda y.
      if null x then null y
      else if null y then false
      else (hd x = hd y) and (ListEq  tl x  tl y)

in list x st
      not null( list y st ListEq (append x y) (1::(2::nil)) )