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

(exists l (append (cons a nil) (cons b nil) l)).

(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))))))).