α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ ofList (toList l)
α : Type u_1
l : Lists' α true
⊢ l ⊆ l
rw [← Lists'.of_toList l]
no goals
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ ofList (toList l)
exact ofList_subset (List.Subset.refl _)