no goals
α : Sort u_1
β : Sort ?u.5647
γ : Sort ?u.5650
p q : α → Prop
a : Subtype p
b : α
⊢ (∃ h, { val := b, property := h } = a) ↔ b = ↑a
simp only [@eq_comm _ b, exists_eq_subtype_mk_iff, @eq_comm _ _ a]