specialize hb x
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : ∀ i ∈ I, b ∈ A i
⊢ b ∈ A x
α β : Type
I J : Set α
A : α → Set β
hsub : J ⊆ I
x : α
hx : x ∈ J
b : β
hb : x ∈ I → b ∈ A x
⊢ b ∈ A x