Composing sumbools for container type

I'm trying to build an equality predicate returning sumbool instead of bool for a simple type:

Inductive state_type : Set := State : nat -> nat -> state_type.

Here's a working solution, which splits into subgoals based on whether the fields match (one at a time).

Definition state_eq : forall (s1 s2 : state_type), {s1 = s2} + {s1 <> s2}.
  intros.
  destruct s1 as [a1 b1]. destruct s2 as [a2 b2].
  destruct (eq_nat_dec a1 a2) as [Aeq | Aneq]. destruct (eq_nat_dec b1 b2) as [Beq | Bneq].
  left. congruence.
  right. congruence.
  right. congruence.
Defined.

The proof is readable, but I'd like a more direct proof using refine:

Definition state_eq2 : forall (s1 s2 : state_type), {s1 = s2} + {s1 <> s2}.
  refine (fun (s1 s2 : state_type) =>
            match s1, s2 with State a1 b1, State a2 b2 =>
               if (eq_nat_dec a1 a2)
               then if (eq_nat_dec b1 b2)
                    then left _ _
                    else right _ _
               else right _ _
            end).
Defined.

The three return values end up as subgoals, but the context for all of them loses the eq_nat_dec hypotheses, rendering them unprovable. How can I retain these hypotheses to finish the proof?