apply propext
case h
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n = p₂ n
case h.a
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n ↔ p₂ n