rw [List.cons_eq_cons] 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
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a :: xs = x :: (pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf)
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)
α 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
x : { x // x ∈ G.V } ⊕ { x // x ∈ G.Z }
pres : List ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
hpre : step.pre = x :: pres
sound : Sum.inr a = x ∧ xs = pres ++ Sum.inl (Production.ContextFree.lhs_var ↑step.prod) :: step.suf
⊢ x :: pres = Sum.inr a :: List.tail (x :: pres)