--- a/TODO	Mon Jun 20 09:29:42 2011 +0900
+++ b/TODO	Mon Jun 20 09:36:16 2011 +0900
@@ -1,13 +1,23 @@
 Function definitions
 
-- export proofs bout alpha_bn
-- equations like
+- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?
 
+- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]
+
+- equations that talk about True/False, for example
     | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
+  do not work (since 'function' does not work)
 
-  do not work
+- equivariance for functions can be derived automatically (knowing termination and
+  equivariance of the graph).
 
-Parser should check that:
+- for multiple simultanously defined functions, compatibility cases should fold the
+  definition and derive eqvt_at for the folded one
+
+- equivariance of the graph for multiple functions does not use equivariance
+  infrastructure
+
+Nominal_Datatype Parser should check that:
 
 - types of bindings match types of binding functions
 - fsets are not bound in lst bindings
@@ -16,7 +26,7 @@
 
 Smaller things:
 
-- maybe <type>_perm whould be called permute_<type>.simps;
+- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;
   that would conform with the terminology in Nominal2