constructor
case a
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f ↔ x ∈ Set.empty
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty.bind f → x ∈ Set.empty

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.13789
f : α → Set β
x : β
⊢ x ∈ Set.empty → x ∈ Set.empty.bind f