Zulip Chat Archive
Stream: general
Topic: another extensionality lemma?
Scott Morrison (Nov 10 2018 at 06:24):
Any complaints about adding @[extensionality] to subtype.eq?
protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
Scott Morrison (Nov 10 2018 at 06:25):
(deleted)
Last updated: May 02 2025 at 03:31 UTC