ShouldBePi.agda:8,8-15
(x : _3) → _3 !=< One of type Set
when checking that the expression λ x → x has type One