case mk
a b c d : Prop
α : Type u
p : α → Prop
val✝ : α
property✝ : p val✝
h : p { val := val✝, property := property✝ }.val
⊢ { val := { val := val✝, property := property✝ }.val, property := h } = { val := val✝, property := property✝ }
a✝ b c d : Prop
α : Type u
p : α → Prop
a : Subtype fun x => p x
h : p a.val
⊢ { val := a.val, property := h } = a
cases a
no goals
case mk
a b c d : Prop
α : Type u
p : α → Prop
val✝ : α
property✝ : p val✝
h : p { val := val✝, property := property✝ }.val
⊢ { val := { val := val✝, property := property✝ }.val, property := h } = { val := val✝, property := property✝ }
exact rfl