Bug fixing + few more examples

- more precise type for apply(One)
- weaken was creating an infinite loop
- eta expansion of bot-elim was not handled