  Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an
extension of intuitionistic propositional logic by means of the distributivity
scheme K, and of co-reflection $A\rightarrow\Box A$. This way, belief is
interpreted as a result of verification, and it fits an extended
Brouwer-Heyting-Kolmogorov interpretation for intuitionistic propositional
logic with an epistemic modality. In the present paper, structural properties
of a natural deduction system $\mathsf{IEL}^{-}$ for intuitionistic belief are
investigated. The focus is on the analyticity of the calculus, so that the
normalization theorem and the subformula property are proven firstly. From
these, decidability and consistency of the logic follow as corollaries.
Finally, disjunction properties, $\Box$-primality, and admissibility of
reflection rule are established by using purely proof-theoretic methods.
