 This fundamental result, roughly expressing the rule \((\rightarrow I)\) of \(\mathbf{I},\) can be proved for \(\mathbf{H–IQC}\) by induction on the definition of a derivation. The other rules of \(\mathbf{I}\) hold for \(\mathbf{H–IQC}\) essentially by modus ponens, which corresponds to \((\rightarrow E)\) in \(\mathbf{N–IQC};\) and all the axioms of \(\mathbf{H–IQC}\) are provable in \(\mathbf{N–IQC}.\)