case h.e'_3.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ l = reverse (reverse l)
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ next (reverse l) x (_ : x ∈ reverse l) = prev l x hx
convert (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x ((mem_reverse _ _).mpr hx)).symm
no goals
case h.e'_3.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ l = reverse (reverse l)
exact (reverse_reverse l).symm