case a.isFalse nab =>
  simp
  rw [String.decEq_refl a]; simp
  apply S_induction; intros m; simp
  rw [String.decEq_refl b]; simp
  induction n <;> induction m <;> simp at *
  case a.zero.zero =>
    constructor <;> constructor <;> constructor
  case a.zero.succ n ih =>
    rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
    constructor <;> try constructor <;> try constructor <;> try assumption
    simp at *
  case a.succ.zero n ih =>
    rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
    constructor <;> try constructor <;> try constructor <;> try assumption
    simp at *
  case a.succ.succ n m ihn ihm =>
    sorry
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    match isFalse nab 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 nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isFalse nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
no goals