∀ {α : Type u_1}
  (motive :
    (s1 s2 : Stream'.Seq α) → (∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) → Prop)
  (s1 s2 : Stream'.Seq α) (h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)),
  (∀ (s : Stream'.Seq α) (S T : Stream'.Seq (Stream'.Seq1 α)),
      motive (s.append (S.append T).join) (s.append (S.join.append T.join)) ⋯) →
    motive s1 s2 h