axiom P : Prop → Prop

@[congr]
axiom P_congr (a b : Prop) (h : a ↔ b) : P a ↔ P b

theorem ex1 {p q : Prop} (h : p ↔ q) (h' : P q) : P p := by
  simp [h]
  assumption

#print ex1

theorem ex2 {p q : Prop} (h : p = q) (h' : P q) : P p := by
  simp [h]
  assumption

#print ex2