Dennis H (Mar 20 2023 at 08:25): 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...
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: Oct 04 2023 at 19:01 UTC