twee-0.1: tests/append-rev.p

cnf(a, axiom, rev(rev(X)) = X).
cnf(a, axiom, '++'(X,'++'(Y,Z)) = '++'('++'(X,Y),Z)).
cnf(a, axiom, '++'(rev(X),rev(Y)) = rev('++'(Y,X))).
cnf(a, axiom, '++'(a,rev(b)) != rev('++'(b, rev(a)))).