Isaac Freund (Oct 01 2022 at 09:16): Isaac Freund (Oct 01 2022 at 09:16):Hello, I have a subgoal containing a ∀x::Foo. ... expression and know that Foo only has one possible value. In the past I've used apply(case_tac x) to handle a similar situation, but it seems that does not work with ∀x::Foo. ..., only with ⋀x::Foo. ....
Isaac Freund (Oct 01 2022 at 09:17):Is there a way to convert ∀x::Foo. ... to ⋀x::Foo. ... or otherwise cleanly solve this?
Jan van Brügge (Oct 01 2022 at 09:52):you can use rule allI to get rid of the HOL forall
Wolfgang Jeltsch (Oct 01 2022 at 13:31):Also, if possible, use cases instead of case_tac, as the former is more high-level than the latter.
Last updated: Dec 21 2024 at 16:20 UTC