Additional congruence lemmas.

theorem imp_congr_eq {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d)

theorem imp_congr_ctx_eq {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a → b) = (c → d)

theorem eq_true_intro {a : Prop} (h : a) : a = True

theorem eq_false_intro {a : Prop} (h : ¬a) : a = False

theorem Iff.to_eq {a : Prop} {b : Prop} (h : a ↔ b) : a = b

theorem iff_eq_eq {a : Prop} {b : Prop} : (a ↔ b) = (a = b)