constructor <;> simp <;> try rw [String.decEq_refl a] <;> apply NoVars.fromNat
case a
a : String
n : ℕ
⊢ Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
case a.a
a : String
n : ℕ
⊢ Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat))) =
    Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat)))