Index: tests/avltree/avl0.c
===================================================================
--- tests/avltree/avl0.c	(revision 90152a4860529aff7214be01cd22abd37012cd19)
+++ tests/avltree/avl0.c	(revision 90152a4860529aff7214be01cd22abd37012cd19)
@@ -0,0 +1,11 @@
+#include "avl.h"
+
+forall(otype T | Comparable(T))
+int ?==?(T t1, T t2) {
+  return !(t1 < t2) && !(t2 < t1);
+}
+
+forall(otype T | Comparable(T))
+int ?>?(T t1, T t2) {
+  return t2 < t1;
+}