no goals
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₁ l₂ : List α
f : α → m PUnit
⊢ List.forM (l₁ ++ l₂) f = do
    List.forM l₁ f
    List.forM l₂ f
induction l₁ <;> simp [*]