Zulip Chat Archive
Stream: new members
Topic: forall
Ashvni Narayanan (Jul 03 2020 at 23:58):
I have a goal of the form:
a : ∀ (x : ℤ), n < x
⊢ false
How can I solve this? Simp does not do it.
Any help is appreciated. Thank you!
Mario Carneiro (Jul 04 2020 at 00:00):
specialize a n
Ashvni Narayanan (Jul 04 2020 at 00:03):
That works, thanks!
Last updated: May 02 2025 at 03:31 UTC