Issue279.agda:20,10-12 The constructor tt does not construct an element of ⊥ when checking that the expression tt has type ⊥