fsplit with name

Stream: general

[Reid Barton]

I want to construct an Exists value where both parts are Props in tactic mode. Is there a convenient way to use something like fsplit to produce two subgoals but also to have the result of the first subgoal available as a hypothesis in the second subgoal?

[Reid Barton]

Currently I have have : P, { ... }, refine <this, _>, ... but it's a little clunky and it means I have to write out P

[Reid Barton]

actually I turned out not to need this, but I'm still curious