See also Löb’s theorem: https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem

Compare Löb’s theorem with the signature of `loeb` with some renaming to make them match up:

> in any formal system F, for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F

    loeb :: Functor f => f (f p -> p) -> f p

To see it even better, look at the section that introduces the modal logic operator (the square that operates on formulae).