constructor
case a.mp.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f ∧ g' y ∈ (fun f => Set.map f s) (g' ∘ f')
case a.mp.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f

case a.mp.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ g' y ∈ (fun f => Set.map f s) (g' ∘ f')