Theorem: Languages.thm_3_c (FOL/Parsing/Text.lean)

State before:
α : Type
L1 L2 L3 : Language α
⊢ concat L1 (concat L2 L3) = concat (concat L1 L2) L3
Tactic:
simp only [concat]
State after:
α : 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}

State before:
α : 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}
Tactic:
simp
State after:
no goals