[GOAL]
α : Type u_1
⊢ List α ≃ DList α
[PROOFSTEP]
refine'
  { toFun := DList.ofList
    invFun := DList.toList .. }
[GOAL]
case refine'_1
α : Type u_1
⊢ LeftInverse toList ofList
[PROOFSTEP]
simp [Function.RightInverse, Function.LeftInverse, DList.toList_ofList, DList.ofList_toList]
[GOAL]
case refine'_2
α : Type u_1
⊢ Function.RightInverse toList ofList
[PROOFSTEP]
simp [Function.RightInverse, Function.LeftInverse, DList.toList_ofList, DList.ofList_toList]
