unfold IndView.toList1 toIndView
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ (IndView.pure x).toList1 = List1.cons y [] ↔ (List1.cons y []).toIndView = IndView.pure x
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] ↔ IndView.pure y = IndView.pure x