we should implement a library of exercise tasks because of two reasons. The first reason is we have the possibility to do some more test for our proofchecker. the second reason is the user can start using our tool to exercise even without external tasks.