apply vw_nin_l
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ False
α : Type u_1
L : Language α
u v w : Word α
uw_in_l : u * w ∈ L
vw_nin_l : v * w ∉ L
contra : u ≃( L ) v
⊢ v * w ∈ L