3.9 so
The so data type is a predicate on Bool which guarantees that the value is true:

data so : Bool -> Type where
    oh : so True

This is most useful for providing a static guarantee that a dynamic check has been made. For example, we
might provide a safe interface to a function which draws a pixel on a graphical display as follows, where
so (inBounds x y) guarantees that the point (x,y) is within the bounds of a 640 × 480 window:

inBounds : Int -> Int -> Bool
inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
drawPoint x y p = unsafeDrawPoint x y

ле к