∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : List α}
  {f : α → m (Option β)}, List.filterMapM f (wfParam xs) = List.filterMapM f xs.attach.unattach