Updated definitions in 5_typed

All definitions in tutorial/1_k/5_typed kompile now, but there seem to be some bugs in the fixes that @traiansf made and thus ktest does not pass the tests.  Nevertheless, all changes here were quite mechanical, so there should be absolutely no problem once unification.k and/or substitution.k get fixed.  For that reason, I made this into a pull request.