Theorem: List.intercalate_singleton (One.lean)

State before:
α : Type u_1
sep elem : List α
⊢ intercalate sep [elem] = elem
Tactic:
rw [List.intercalate, List.intersperse_singleton, List.join_cons, List.join_nil, List.append_nil]
State after:
no goals