simp at this
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w * ε ∈ L ↔ v * w * ε ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L
case mpr
α : Type u_1
L : Language α
u v : Word α
h : ∀ (x : Word α), u * x ≃( L ) v * x
w : Word α
this : u * w ∈ L ↔ v * w ∈ L
⊢ u * w ∈ L ↔ v * w ∈ L