rw [String.decEq_refl a]
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
a : String
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O