Stream: Beginner Questions

Topic: ✔ Prove ∃x::A. P x ⟹ ∃x::'a P x

Isaac Freund (Oct 17 2022 at 10:45):

Is it possible to prove a subgoal of the form ∃x::A. P x ⟹ ∃x::'a P x or do I need to restructure earlier parts of my proof?

Isaac Freund (Oct 17 2022 at 10:56):

Nevermind, it looks like the reason sledgehammer wasn't able to solve my concrete subgoal lay elsewhere. Sorry for the noise.

Notification Bot (Oct 17 2022 at 10:56):

Isaac Freund has marked this topic as resolved.

Last updated: Apr 19 2024 at 12:27 UTC