no goals
α : Type u_1
β : Type u_2
γ : Type ?u.269744
ι : Sort ?u.269747
ι' : Sort ?u.269750
ι₂ : Sort ?u.269753
κ : ι → Sort ?u.269758
κ₁ : ι → Sort ?u.269763
κ₂ : ι → Sort ?u.269768
κ' : ι' → Sort ?u.269773
s : Set (α → β)
a : α
⊢ ∀ (x : β), x ∈ seq s {a} ↔ x ∈ (fun f => f a) '' s
simp