constructor
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a
case left
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ X, f x = a

case right
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ Y, f x = a