Understanding higher-order code (Haskell)

> Ignoring ⊥, in all forms, we can see that there's only a proof that's isomorphic to any given proof, namely the same given proof. In other words, the only program implements a → a is the identity:

It doesn't necessarily follow that the program is the identity for all types: it could be the identity for all types but, say, Int, where instead it returns 5. In Haskell this is not possible without FlexibleInstances, but we haven't assumed that property of the types-as-theorems model. (To interpret things literally, if I imagine a computer where I type in a proof of something and it prints out a proof of the same thing, I don't intuitively expect that it can't introspect on what I typed in.)