contradiction
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
hh : x = y
ht : [] = head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
no goals