have ⟨_, h⟩ := Production.lhs_contains_var step.prod.val
α 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]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ 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]
head✝ : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
tail✝ : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = head✝ :: tail✝
tmp✝ : head✝ = Sum.inl v ∧ tail✝ = [] ∧ Production.lhs ↑step.prod = [] ∧ step.suf = []
tmp : Production.lhs ↑step.prod = []
w✝ : { x // x ∈ G.V }
h : Sum.inl w✝ ∈ Production.lhs ↑step.prod
⊢ Production.lhs ↑step.prod = [Sum.inl v] ∧ head✝ :: tail✝ = ε ∧ step.suf = ε