 Kripke models for languages with equality may interpret \(=\) at each node by an arbitrary equivalence relation, subject to monotonicity. For applications to intuitionistic arithmetic, normal models (those in which equality is interpreted by identity at each node) suffice because equality of natural numbers is decidable.