Stream: new members
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 10 2021 at 00:31 UTC