simp at this
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u * ε ∈ L ↔ v * ε ∈ L
⊢ u ∈ L ↔ v ∈ L
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
this : u ∈ L ↔ v ∈ L
⊢ u ∈ L ↔ v ∈ L