twee-2.3.1: tests/append-rev-ascii.p

fof(rev_rev, axiom, ![X]: rev(rev(X))=X).
fof(app_assoc, axiom, ![X, Y, Z]: '++'(X, '++'(Y, Z))='++'('++'(X, Y), Z)).
fof(rev_app, axiom, ![X, Y]: '++'(rev(X), rev(Y))=rev('++'(Y, X))).
fof(conjecture, conjecture, '++'(a, rev(b))=rev('++'(b, rev(a)))).