mathlib3 documentation

core / init.propext

@[ext]
constant propext {a b : Prop} :
(a b) a = b

Additional congruence lemmas. #

theorem forall_congr_eq {a : Sort u} {p q : a Prop} (h : (x : a), p x = q x) :
( (x : a), p x) = (x : a), q x
theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) :
(a b) = (c d)
theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c b = d) :
(a b) = (c d)
theorem eq_true_intro {a : Prop} (h : a) :
theorem eq_false_intro {a : Prop} (h : ¬a) :
theorem iff.to_eq {a b : Prop} (h : a b) :
a = b
theorem iff_eq_eq {a b : Prop} :
(a b) = (a = b)