  This paper studies the relationship between labelled and nested calculi for
propositional intuitionistic logic, first-order intuitionistic logic with
non-constant domains and first-order intuitionistic logic with constant
domains. It is shown that Fitting's nested calculi naturally arise from their
corresponding labelled calculi--for each of the aforementioned logics--via the
elimination of structural rules in labelled derivations. The translational
correspondence between the two types of systems is leveraged to show that the
nested calculi inherit proof-theoretic properties from their associated
labelled calculi, such as completeness, invertibility of rules and cut
admissibility. Since labelled calculi are easily obtained via a logic's
semantics, the method presented in this paper can be seen as one whereby
refined versions of labelled calculi (containing nested calculi as fragments)
with favourable properties are derived directly from a logic's semantics.
