case nil
α : Type u_1
⊢ toList (ofList []) = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
α : Type u_1
l : List α
⊢ toList (ofList l) = l
cases l
case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
case nil
α : Type u_1
⊢ toList (ofList []) = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
rfl
no goals
case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
simp only [DList.toList, DList.ofList, List.cons_append, List.append_nil]