  We revisit the notion of intuitionistic equivalence and formal proof
representations by adopting the view of formulas as exponential polynomials.
  After observing that most of the invertible proof rules of intuitionistic
(minimal) propositional sequent calculi are formula (i.e. sequent) isomorphisms
corresponding to the high-school identities, we show that one can obtain a more
compact variant of a proof system, consisting of non-invertible proof rules
only, and where the invertible proof rules have been replaced by a formula
normalisation procedure.
  Moreover, for certain proof systems such as the G4ip sequent calculus of
Vorob'ev, Hudelmaier, and Dyckhoff, it is even possible to see all of the
non-invertible proof rules as strict inequalities between exponential
polynomials; a careful combinatorial treatment is given in order to establish
this fact.
  Finally, we extend the exponential polynomial analogy to the first-order
quantifiers, showing that it gives rise to an intuitionistic hierarchy of
formulas, resembling the classical arithmetical hierarchy, and the first one
that classifies formulas while preserving isomorphism.
