finally? fixing the bug with set_telescope
Added the Whnf vernacular command
small cleanup
fixing an equality bug and a whnf bug
A new example with dependent types and reductions when type-checking