 (Depending on details, further reductions may be needed within the new subproof.) To avoid such detours, we instead use indirect proof to obtain \(D\). This fix, a classicizing reduction, is analogous to the permutative reductions discussed above. The new indirect proof subproof will have \(\neg D\) as its hypothesis; since \(D\) is immediately derivable (by an elimination rule!) from \(C\), we can use \(\neg\)-Int to infer \(\neg C\), after which the argumentation of the original subproof will yield a contradiction.