simp at h₁ h₂
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : π₁ (opair x y) = π₁ (opair z w)
h₂ : π₂ (opair x y) = π₂ (opair z w)
⊢ x = z ∧ y = w
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
h : opair x y = opair z w
h₁ : x = z
h₂ : y = w
⊢ x = z ∧ y = w