cases singl_inter.left
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
⊢ False
case inl
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl = u * w
⊢ False

case inr
α : Type u_1
L : Language α
u v : Word α
pre : u ≠ v
w singl : Word α
singl_inter : singl ∈ {u * w, v * w} ∩ L
h : ∀ v_1 ∈ {u * w, v * w} ∩ L, v_1 = singl
contra : u ≃( L ) v
h2 : u * w ∈ L ↔ v * w ∈ L
h✝ : singl ∈ {v * w}
⊢ False