rcases hx with ⟨j, ⟨hj, hxj⟩⟩
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
hx : ∃ i ∈ J, x ∈ A i
⊢ ∃ i ∈ I, x ∈ A i
case intro.intro
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ ∃ i ∈ I, x ∈ A i