In Intuitionistic Propositional Logic (IPL), the law of excluded middle $P \lor \neg P$ does not generally hold. However, some double-negation variants are valid. Which of the following formulas is intuitionistically valid (i.e., holds in all Heyting algebras)?