simp only [mem_rcomp_iff]
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ z✝ ∈ rcomp (rcomp t s) r ↔ z✝ ∈ rcomp t (rcomp s r)
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ (∃ a b c,
      z✝ = opair a c ∧ (∃ a b_1 c_1, opair b c = opair a c_1 ∧ opair b_1 c_1 ∈ t ∧ opair a b_1 ∈ s) ∧ opair a b ∈ r) ↔
    ∃ a b c, z✝ = opair a c ∧ opair b c ∈ t ∧ ∃ a_1 b_1 c, opair a b = opair a_1 c ∧ opair b_1 c ∈ s ∧ opair a_1 b_1 ∈ r