## 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 15 2021 at 00:39 UTC