exact hsub hj
case h.left
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ j ∈ I

case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j
case h.right
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : β
j : α
hj : j ∈ J
hxj : x ∈ A j
⊢ x ∈ A j