 The fact that ⊢ is an →-introductive extension of ⊢I L suffices for ⊢ to be ∨-classical, and in particular for it to be ‘∨-eliminative’ in the sense that whenever Γ ⊢ χ1 ∨ χ2 and also Γ′, χ1 ⊢ θ and Γ′′, χ2 ⊢ θ, we have Γ, Γ′, Γ′′ ⊢ θ. Thus from the fact that φ ⊢ ψ ∨ (φ # ψ), inset on the right above, and that φ # ψ ⊢ φ → ¬ψ, we may conclude that φ ⊢ ψ ∨ (φ → ¬ψ). Not only does this fail—e.g., with the schematic letters replaced by distinct propositional variables—for ⊢I L, making the extension non-conservative, it takes us all the way to ⊢CL, as claimed in the general formulation ((i) and (ii)) of the result. To see this most easily in the present case, take φ as ⊤.