case a.succ n ih =>
  rw [String.decEq_refl a] at *; simp at *
  cases ih
  case S_axiom_neg nv1 nv2 e =>
    constructor <;> try constructor <;> try assumption
    intros p
    contradiction
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
no goals