  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 also in the light of categorical semantics. 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.
