diff -r a4743b7cd887 -r f65564bcf342 TODO --- a/TODO Sat Mar 20 16:27:51 2010 +0100 +++ b/TODO Sat Mar 20 18:16:26 2010 +0100 @@ -24,10 +24,10 @@ - strong induction rules -- show support equations +- check support equations for more bindings per constructor - automate the proofs that are currently proved with sorry: - alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp + alpha_equivp, fv_rsp, alpha_bn_rsp - store information about defined nominal datatypes, so that it can be used to define new types that depend on these