constructor
case a
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) ↔ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)
case a.mp
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ (y ∈ f.bind fun f => Set.map f (s.insert a)) → y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_2
f : Set (α → β)
a : α
s : Set α
y : β
⊢ y ∈ (Set.map (fun f => f a) f).union (f.bind fun f => Set.map f s) → y ∈ f.bind fun f => Set.map f (s.insert a)