no goals
α : Type u_4
α' : Type ?u.39768
β : Type u_5
β' : Type ?u.39774
γ : Type u_3
γ' : Type ?u.39780
δ : Type u_2
δ' : Type ?u.39786
ε : Type u_1
ε' : Type u_6
ζ : Type ?u.39795
ζ' : Type ?u.39798
ν : Type ?u.39801
f✝ f'✝ : α → β → γ
g✝ g'✝ : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ image2 f (image2 g s t) u = image2 f' s (image2 g' t u)
simp only [image2_image2_left, image2_image2_right, h_assoc]