Zulip Chat Archive
Stream: general
Topic: iff.em?
Yury G. Kudryashov (Sep 24 2021 at 20:17):
What do you think about this dot-notation lemma?
lemma iff.em {p q : Prop} (h : p ↔ q) : (p ∧ q) ∨ (¬p ∧ ¬q)
Yaël Dillies (Sep 24 2021 at 20:33):
Sounds fun!
Last updated: May 02 2025 at 03:31 UTC