> Essentially, true statements are expressions that pass the "type check" of a compiler. A function taking type A as param and returning type B is an implication A->B. To prove this implication, you need to find a function implementation that passes the corresponding type checks. This is what I would have wanted the tutorial to say at the start.

This sounds like the tutorial was geared toward those already familiar with other proof assistants, since this concept is present in most proof assistants.