intro ⟨h, hp⟩
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
⊢ y ∈ (f a).inter (Set.const p) → y ∈ (Set.pureIf a p).bind f
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6883
a : α
p : Prop
f : α → Set β
y : β
h : y ∈ f a
hp : y ∈ Set.const p
⊢ y ∈ (Set.pureIf a p).bind f