unreachable code was reached on some machines

[fpvandoorn]

In the commit d38979f 'unreachable' code was reached when elaborating this theorem on some machines:

lean2/hott/types/trunc.hlean

Line 299 in d38979f

theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) :=

I worked around it by rewriting the proof in the two commits after that.

This error occurred on a machine with Ubuntu 17.04 with g++ 6.3.0 or with g++ 5.4.1 (I believe) and on a mac (with unknown version gcc/g++).

There were no errors on a machine with Ubuntu 16.04 with gcc 5.4.0/g++ 5.4.0