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: Dec 20 2023 at 11:08 UTC