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