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" ch

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.