errors/ShouldBePi.agda:8,8-15
One != (x : _6) -> _7 x of type Set
when checking that the expression \x -> x has type One