intro h w x
case mp
α : Type u_1
L : Language α
u v : Word α
⊢ u ≃( L ) v → ∀ (x : Word α), u * x ≃( L ) v * x
case mp
α : Type u_1
L : Language α
u v : Word α
h : u ≃( L ) v
w x : Word α
⊢ u * w * x ∈ L ↔ v * w * x ∈ L