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