Theorem: Std.AssocList.toList_ofList (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type u_1
β : Type u_2
L : List (α × β)
⊢ toList (ofList L) = L
Tactic:
induction L <;> simp [*]
State after:
no goals