support for dependent types

[c-cube]

• no universes
• must be accepted in typechecking (without inference for term parameters)
• do the encoding (hatt 2016)