rw [String.decEq_refl b]
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)