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