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

State before:
α : Type
L : Language α
⊢ concat L ∅ = ∅
Tactic:
simp only [concat]
State after:
α : Type
L : Language α
⊢ {x | ∃ s ∈ L, ∃ t ∈ ∅, s ++ t = x} = ∅

State before:
α : Type
L : Language α
⊢ {x | ∃ s ∈ L, ∃ t ∈ ∅, s ++ t = x} = ∅
Tactic:
simp
State after:
no goals