[johnnyjeans]

Sorry, I'm rusty enough on my logic that I'll only embarrass myself if I try to match the depth of your post.

> Are there cases where you didn't "obviously" cheat where it's "wrong" to use it?

In particular, it prevents us from adapting the proof to non-binary valued logics full stop.

> I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P.

Now this is an interesting thought.