α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ (destruct s >>= fun x => tail.aux x >>= drop.aux n) = destruct s >>= drop.aux (n + 1)
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ destruct (drop s (n + 1)) = destruct s >>= drop.aux (n + 1)
rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]
no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
n : ℕ
⊢ (destruct s >>= fun x => tail.aux x >>= drop.aux n) = destruct s >>= drop.aux (n + 1)
rfl