simp only [concat]
α : Type
L1 L2 L3 : Language α
⊢ concat L1 (concat L2 L3) = concat (concat L1 L2) L3
α : Type
L1 L2 L3 : Language α
⊢ {x | ∃ s ∈ L1, ∃ t ∈ {x | ∃ s ∈ L2, ∃ t ∈ L3, s ++ t = x}, s ++ t = x} =
    {x | ∃ s ∈ {x | ∃ s ∈ L1, ∃ t ∈ L2, s ++ t = x}, ∃ t ∈ L3, s ++ t = x}