Actually, there *are* good versions of sequent calculus with
equality. Jean-Yves Girard and Peter Schroeder-Heister have both given
the appropriate rules. So, given a language of terms with some
equational theory, the right and left rules are:


    —————————— =R
    Γ ⊢ t = t


    ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C)
    —————————————————————————— =L
    Γ, s = t ⊢ C

The premise of the left rule quantifies over a *complete set of
unifiers* for s and t. For terms freely generated by some signature,
there is a single most general unifier (if one exists), and so the
left rule has at most one premise. Once you add equations then
there can be more than one most general unifier -- possibly  even
infinite (eg, if terms are lambda-terms modulo beta/eta, as in
higher-order unification).

The Girard/Schroeder-Heister equality is not the same as the Martin-Lof
identity type, but it gives rise to a nicer programming language than raw J
does, since the left rule is invertible. Invertible left rules are what give rise to
pattern matching syntax, and so languages like Agda choose a fragment
where the G/SH rule and J coincide to implement pattern matching.

Agda restricts pattern matching so that an identity type
argument can only have a refl pattern when the two terms being equated
are generated from variables and constructors. So an identity proof
p : (cons x y) = (cons a b)) can be matched as refl, but an identity
proof q : (append x y) = (append a b)) can't be.

This restriction ensures that first-order unification suffices for the
G/SH elim, and therefore to implement pattern matching.

If you are very interested in this topic, Joshua Dunfield and I have a draft
paper where we work out the Curry-Howard story for pattern matching
with the G/SH equality (what are called GADTs by PL theorists) in gory
detail:

  Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism and Indexed Types
  <http://www.cl.cam.ac.uk/~nk480/gadt.pdf>

--
Neel Krishnaswami
nk...@cl.cam.ac.uk