induction d1 with
| same h => exact h ▸ d2
| step l _ sound ih => exact step l (ih d2) sound
α 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 })
d1 : Derivation G u v
d2 : Derivation G v w
⊢ Derivation G u w
no goals