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

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

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