cases w
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
w : Word { x // x ∈ G.Z }
xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h_rhs : Sum.inr a :: xs = Sum.inr <$> w
h : lhs = rhs
⊢ w = a :: List.tail w
case nil
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
h_rhs : Sum.inr a :: xs = Sum.inr <$> []
⊢ [] = a :: List.tail []

case cons
α nt : Type
P : Finset α → Finset nt → Type
i : Production.ContextFree α nt P
G : Grammar P
lhs rhs xs : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
a : { x // x ∈ G.Z }
d : Grammar.Derivation G lhs rhs
h_lhs : lhs = Sum.inr a :: xs
h : lhs = rhs
head✝ : { x // x ∈ G.Z }
tail✝ : List { x // x ∈ G.Z }
h_rhs : Sum.inr a :: xs = Sum.inr <$> (head✝ :: tail✝)
⊢ head✝ :: tail✝ = a :: List.tail (head✝ :: tail✝)