pred 3 append. 
pred 2 equal.
term 0 nil.    
term 2 cons.   
term 0 a, b.

(forall l ((append l (cons b nil) (cons a (cons b nil))) => 
                     (equal l (cons a nil)))).

(forall l (append nil l l)).

(forall l (forall k (forall m (forall x 
  ((append l k m) => (append (cons x l) k (cons x m))))))).

(forall x (equal x x)).