rw [←hxt]
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P t
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P x