simp_rw [hpre, HMul.hMul, Mul.mul] at sound
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
sound : Sum.inr a :: xs = step.pre * [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)] * step.suf
hpre : step.pre = []
⊢ [] = Sum.inr a :: List.tail []
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
step : Grammar.DerivationStep G lhs
h_lhs : lhs = Sum.inr a :: xs
hpre : step.pre = []
sound : Sum.inr a :: xs = List.append (List.append [] [Sum.inl (Production.ContextFree.lhs_var ↑step.prod)]) step.suf
⊢ [] = Sum.inr a :: List.tail []