pred 3 append.
pred 2 equal.
term 0 nil.
term 2 cons.
term 0 a, b.
(forall l (forall k ((append nil l k) => (equal l k)))).
(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)).