Zulip Chat Archive

Stream: new members

Topic: to_Prop_inj

Kenny Lau (Jan 11 2019 at 10:31):

lemma to_Prop_inj : Π {a b : bool} (H : (a : Prop) ↔ (b : Prop)), a = b
| a tt H := H.2 rfl
| a ff H := bool.eq_ff_of_ne_tt $ λ h, absurd (H.1 h) dec_trivial

Kenny Lau (Jan 11 2019 at 10:31):

@Mario Carneiro is this currently in mathlib?

Last updated: May 02 2025 at 03:31 UTC