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

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