So in a proof I have an assumption of the form `h : ∃ l : M ⟦ b, x ⟧, P(l)`

for some `P`

of appropriate type, and I need to prove something of the form `∃ l : M ⟦ a, x ⟧, P(l)`

. I noticed I could `apply hinhpr.`

to turn my goal into a normal `∑`

statement, but how can I extract `l`

from `h`

? I can't just `destruct`

like I would with a normal `∑`

type...

I got it to work with `unshelve eapply (hinhuniv _ h).`

, but I am not sure if this is the best strategy, if anyone has better suggestions, please let me know!

Last updated: Oct 04 2023 at 19:01 UTC