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