simp only [mem_sep_iff, interpret_memRComp', interpret_inr, interpret_inl, ite_true, ite_false,
  and_iff_right_iff_imp, forall_exists_index, and_imp]
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈
      sep (BoundedFormula.memRComp (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then s else r)
        (prod (dom r) (ran s)) ↔
    ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ prod (dom r) (ran s)