α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ Seq.join
      ((fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s)) <$>
        Seq.cons none S) =
    Seq.cons none
      (Seq.join
        ((fun o =>
            match o with
            | none => Seq1.ret none
            | some s => (none, s)) <$>
          S))
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ join (think S) = think (join S)
simp [think, join]
no goals
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ Seq.join
      (Seq.map
        (fun o =>
          match o with
          | none => Seq1.ret none
          | some s => (none, s))
        (Seq.cons none S)) =
    Seq.cons none
      (Seq.join
        (Seq.map
          (fun o =>
            match o with
            | none => Seq1.ret none
            | some s => (none, s))
          S))
simp [join, Seq1.ret]