Zulip Chat Archive
Stream: new members
Topic: reversing `\neq`
Scott Morrison (Feb 24 2019 at 06:26):
If I have h : ¬(a=b), what's the canonical name for ¬(b=a)?
Mario Carneiro (Feb 24 2019 at 08:02):
ne.symm h
Mario Carneiro (Feb 24 2019 at 08:03):
If h is literally a ne you can use projection notation
Last updated: May 02 2025 at 03:31 UTC