aesop
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ y z,
    interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
      opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
no goals