Zulip Chat Archive
Stream: general
Topic: equality of proofs
Reid Barton (Apr 28 2018 at 02:22):
Is this lemma true and what is it (or should it be) called?
lemma hpropext {p q : Prop} (a : p) (b : q) : a == b := sorry
Reid Barton (Apr 28 2018 at 02:26):
proof_irrel is the non-heterogeneous version
Reid Barton (Apr 28 2018 at 02:29):
OK, I managed to prove it
Last updated: May 02 2025 at 03:31 UTC