induction d with
| same h => apply same; simp [h]
| step s _ sound =>
  apply step
  . assumption
  swap
  . exact s.augment_left w
  . rw [<- sound]; exact s.augment_left_result _
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝ u v w : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
d : Derivation G u v
⊢ Derivation G (w * u) (w * v)
no goals