--- a/TODO	Tue May 10 17:10:22 2011 +0100
+++ b/TODO	Fri May 13 14:50:17 2011 +0100
@@ -1,7 +1,11 @@
 Function definitions
 
 - export proofs bout alpha_bn
+- equations like
 
+    | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
+
+  do not work
 
 Parser should check that: