We provide a natural formulation of the sequent calculus with equality and establish the cut elimination theorem. We also briefly comment on its applications to the logic of partial terms, when "existence" is formulated as equality with a (bound) variable
