Elimination and Uniqueness Principle for the Unit Type