Or it might be that formal Math notation is not for me.

No, it just means that you haven't studied that notation. Like programming, being skilled at maths is not something you're just naturally gifted with. It has to be studied.

The proof of the proposition in question is "trivial" in the sense that a first course in formal logic is more than enough to fully understand it, and that there is really no extra trick involved, basically the proof is as straightforward as it could be.

I will agree that the article doesn't explain enough how the formula in question relates to type theory and Rust's type system in particular.