Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: ideas for exercises
Jalex Stark (May 17 2020 at 16:30):
using rw under a universal quantifier should "just" require introing and reverting
Last updated: May 02 2025 at 03:31 UTC
using rw under a universal quantifier should "just" require introing and reverting
Last updated: May 02 2025 at 03:31 UTC