unfold Grammar.DerivationStep.result at r
α 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 : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : Grammar.DerivationStep.result s = u'✝
⊢ w = a :: List.tail 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 : rhs = Sum.inr <$> w
u'✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : Grammar.DerivationStep G lhs
d : Grammar.Derivation G u'✝ rhs
r : s.pre * Production.rhs ↑s.prod * s.suf = u'✝
⊢ w = a :: List.tail w