 is admissible for intuitionistic propositional logic \(\mathbf{IPC}\) because if \(A,\) \(B\) and \(C\) are any formulas such that \(\neg A \rightarrow(B \vee C)\) is provable in \(\mathbf{IPC},\) then \((\neg A \rightarrow B) \vee (\neg A \rightarrow C)\) is provable in \(\mathbf{IPC}.\) Harrop’s rule is not derivable in \(\mathbf{IPC}\) because the formula