Stream: Coq users

Topic: Proof strategy for UniMath `hexists` statements


view this post on Zulip Dennis H (Mar 20 2023 at 08:25):

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...

view this post on Zulip Dennis H (Mar 20 2023 at 08:43):

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: Mar 28 2024 at 13:01 UTC