case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.275320
ι' : Sort ?u.275323
ι₂ : Sort ?u.275326
κ : ι → Sort ?u.275331
κ₁ : ι → Sort ?u.275336
κ₂ : ι → Sort ?u.275341
κ' : ι' → Sort ?u.275346
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ seq (f '' s) t
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.275320
ι' : Sort ?u.275323
ι₂ : Sort ?u.275326
κ : ι → Sort ?u.275331
κ₁ : ι → Sort ?u.275336
κ₂ : ι → Sort ?u.275341
κ' : ι' → Sort ?u.275346
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = seq (f '' s) t
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.275320
ι' : Sort ?u.275323
ι₂ : Sort ?u.275326
κ : ι → Sort ?u.275331
κ₁ : ι → Sort ?u.275336
κ₂ : ι → Sort ?u.275341
κ' : ι' → Sort ?u.275346
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ seq (f '' s) t
simp