have ⟨h, _⟩ := h
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
v : { x // x ∈ G.V }
step : DerivationStep G [Sum.inl v]
hpre : step.pre = []
h✝ : Production.lhs ↑step.prod = ε ∧ step.suf = [Sum.inl v]
w✝ : { x // x ∈ G.V }
c : Sum.inl w✝ ∈ Production.lhs ↑step.prod
h : Production.lhs ↑step.prod = ε
right✝ : step.suf = [Sum.inl v]
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ [] = ε ∧ step.suf = ε