toprove_ :: Note -> Note
toprove_ n = todo $ do
    n
    newline
    "There is a proof missing here."
toprove_ :: Note -> Note
toprove_ n = todo $ do
    n
    newline
    "There is a proof missing here."
toprove_ n = todo $ do
    n
    newline
    "There is a proof missing here."