Theorem: nullable_emptyStr' (Katydid/Conal/Calculus.lean)

State before:
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ ν' ε
Tactic:
constructor
State after:
case a
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ [] = []

State before:
case a
x✝¹ : Type
x✝ : PUnit.{u_1}
⊢ [] = []
Tactic:
rfl
State after:
no goals