unfold IndView.toList1 toIndView
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ (IndView.cons x xs).toList1 = List1.cons y (head✝ :: tail✝) ↔
    (List1.cons y (head✝ :: tail✝)).toIndView = IndView.cons x xs
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (head✝ :: tail✝) ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs