. rw [<- sound]; exact s.augment_left_result _
case step.sound
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ u'✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
s : DerivationStep G u✝
x✝ : Derivation G u'✝ v✝
sound : DerivationStep.result s = u'✝
x_ih✝ : Derivation G (w * u'✝) (w * v✝)
⊢ DerivationStep.result (DerivationStep.augment_left s w) = w * u'✝
no goals