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 x and not null( list y st ListEq (append x y) (1::(2::nil)) ) and not null( list z st ListEq (append x y) (2::(2::nil)) )