TODO
2010-03-18 Christian Urban added item about size functions
2010-03-18 Cezary Kaliszyk Continued description of alpha.
2010-03-18 Cezary Kaliszyk Added fv,bn,distinct,perm to the simplifier.
2010-03-18 Cezary Kaliszyk fv_bn may need to call other fv_bns.
2010-03-18 Cezary Kaliszyk Update TODO.
2010-03-18 Cezary Kaliszyk Which proofs need a 'sorry'.
2010-03-18 Christian Urban added TODO
less more (0) tip