simp [h]
case same.h
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u✝¹ u v w u✝ v✝ : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
h : u✝ = v✝
⊢ w * u✝ = w * v✝
no goals