match d with
| .same h =>
  rw [<- h, h_lhs] at h_rhs
  cases w
  simp [List.map_nil] at h_rhs
  simp [List.map_cons] at h_rhs
  rw [List.cons_eq_cons] at h_rhs
  have _ := (Sum.inr_injective h_rhs.left).symm
  simp; rw [List.cons_eq_cons]
  simp; assumption
| .step s d r =>
  unfold Grammar.DerivationStep.result at r
  rw [ContextFreeGrammar.derivation_step_prefix s h_lhs] at r
  simp_rw [HMul.hMul, Mul.mul] at r
  simp at r
  let h_lhs' := r.symm
  exact ContextFreeGrammar.derivation_preserves_prefix d h_lhs' h_rhs
α 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
⊢ w = a :: List.tail w
no goals