Sometimes when I'm proving something, I have a hypothesis P x y, and I know that I have a definition like R x := exists y, P x y. I would like to add the hypothesis R x, but I don't know how to do it. I tried to use pose proof (R x), but I got something of type Prop. Is there a way to do it?
If you have a hypothesis Hxy: P x y, you can write
assert (Rx: R x) by (exists y; assumption).
On the other direction, if you have a hypothesis Hx: R x, the tactic destruct Hx as [y Pxy] adds the witness yand the corresponding hypothesis to your context.