∀ {α : Type u_2} {β : Type u_1} (R : α → β → Prop) (s1 : Stream'.WSeq β) (s2 : Stream'.WSeq α)
  (motive :
    (∃ s t S T,
        s1 = s.append S.join ∧
          s2 = t.append T.join ∧
            Function.swap (Stream'.WSeq.LiftRel R) s t ∧
              Function.swap (Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R)) S T) →
      Prop)
  (x :
    ∃ s t S T,
      s1 = s.append S.join ∧
        s2 = t.append T.join ∧
          Function.swap (Stream'.WSeq.LiftRel R) s t ∧
            Function.swap (Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R)) S T),
  (∀ (s : Stream'.WSeq β) (t : Stream'.WSeq α) (S : Stream'.WSeq (Stream'.WSeq β)) (T : Stream'.WSeq (Stream'.WSeq α))
      (h1 : s1 = s.append S.join) (h2 : s2 = t.append T.join) (st : Function.swap (Stream'.WSeq.LiftRel R) s t)
      (ST : Function.swap (Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R)) S T), motive ⋯) →
    motive x