Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!
Ah, cool thanks! I also realised that if you were just using the type checker in your head, once you got to (P → ⊥) → ⊥, you could consider your proof done by your (outside of the type checker) assumption of LEM. But I see no we don’t need to assume it outside of the type checker!