intro h
case mp
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ x y z w : V
⊢ 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
⊢ x = z ∧ y = w