cases (String.decEq a b)
case a
a b : String
n : ℕ
⊢ Ø ⋁
    match String.decEq a b with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
case a.isFalse
a b : String
n : ℕ
h✝ : ¬a = b
⊢ Ø ⋁
    match isFalse h✝ with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isFalse h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isFalse h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a

case a.isTrue
a b : String
n : ℕ
h✝ : a = b
⊢ Ø ⋁
    match isTrue h✝ with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isTrue h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isTrue h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a