Comment by rzmmm

You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.