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: Dec 20 2025 at 21:32 UTC
using rw under a universal quantifier should "just" require introing and reverting
Last updated: Dec 20 2025 at 21:32 UTC