α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct = do
    let x ← destruct s
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ destruct (tail s) = destruct s >>= tail.aux
simp [tail]
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (destruct s >>= fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = do
    let x ← destruct s
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (fun o => Option.rec nil Prod.snd o) <$> destruct s >>= destruct = do
    let x ← destruct s
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
rw [← bind_pure_comp, LawfulMonad.bind_assoc]
case h
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = fun x =>
    match x with
    | none => Computation.pure none
    | some (fst, s) => destruct s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (destruct s >>= fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = do
    let x ← destruct s
    match x with
      | none => Computation.pure none
      | some (fst, s) => destruct s
apply congr_arg
no goals
case h
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ (fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = fun x =>
    match x with
    | none => Computation.pure none
    | some (fst, s) => destruct s
ext1 (_ | ⟨a, s⟩) <;> apply (@pure_bind Computation _ _ _ _ _ _).trans _ <;> simp