no goals
α : Type u_1
β : Type ?u.196879
γ : Type ?u.196882
ι : Sort ?u.196885
ι' : Sort ?u.196888
ι₂ : Sort ?u.196891
κ : ι → Sort ?u.196896
κ₁ : ι → Sort ?u.196901
κ₂ : ι → Sort ?u.196906
κ' : ι' → Sort ?u.196911
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ { val := x, property := h } ∈ univ ↔ { val := x, property := h } ∈ ⋃ (x : α) (h : p x), {{ val := x, property := h }}
simp [h]