α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm l * formPerm (reverse l) = 1
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (reverse l) = (formPerm l)⁻¹
rw [eq_comm, inv_eq_iff_mul_eq_one]
case H
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l * formPerm (reverse l)) x = ↑1 x
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm l * formPerm (reverse l) = 1
ext x
case H
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
case H
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l * formPerm (reverse l)) x = ↑1 x
rw [mul_apply, one_apply]
case H.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x

case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
case H
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
cases' Classical.em (x ∈ l) with hx hx
case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
case H.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x

case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
. obtain ⟨k, hk, rfl⟩ := nthLe_of_mem ((mem_reverse _ _).mpr hx)
  have h1 : l.length - 1 - k < l.length := by
    rw [Nat.sub_sub, add_comm]
    exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
  have h2 : length l - 1 - (k + 1) % length (reverse l) < length l := by
    rw [Nat.sub_sub, length_reverse];
    exact Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
      (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
  rw [formPerm_apply_nthLe l.reverse (nodup_reverse.mpr h), nthLe_reverse' _ _ _ h1,
    nthLe_reverse' _ _ _ h2, formPerm_apply_nthLe _ h]
  congr
  rw [length_reverse] at *
  cases' lt_or_eq_of_le (Nat.succ_le_of_lt hk) with h h
  . rw [Nat.mod_eq_of_lt h, ← Nat.sub_add_comm, Nat.succ_sub_succ_eq_sub,
      Nat.mod_eq_of_lt h1]
    exact (Nat.le_sub_iff_add_le (length_pos_of_mem hx)).2 (Nat.succ_le_of_lt h)
  . rw [← h]; simp
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
case H.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem ((mem_reverse _ _).mpr hx)
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
have h1 : l.length - 1 - k < l.length := by
  rw [Nat.sub_sub, add_comm]
  exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
have h2 : length l - 1 - (k + 1) % length (reverse l) < length l := by
  rw [Nat.sub_sub, length_reverse];
  exact Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
    (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ nthLe l ((length l - 1 - (k + 1) % length (reverse l) + 1) % length l)
      (_ : (length l - 1 - (k + 1) % length (reverse l) + 1) % length l < length l) =
    nthLe l (length l - 1 - k) h1
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) (nthLe (reverse l) k hk)) = nthLe (reverse l) k hk
rw [formPerm_apply_nthLe l.reverse (nodup_reverse.mpr h), nthLe_reverse' _ _ _ h1,
  nthLe_reverse' _ _ _ h2, formPerm_apply_nthLe _ h]
case H.inl.intro.intro.e_n
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ (length l - 1 - (k + 1) % length (reverse l) + 1) % length l = length l - 1 - k
case H.inl.intro.intro
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ nthLe l ((length l - 1 - (k + 1) % length (reverse l) + 1) % length l)
      (_ : (length l - 1 - (k + 1) % length (reverse l) + 1) % length l < length l) =
    nthLe l (length l - 1 - k) h1
congr
case H.inl.intro.intro.e_n
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
case H.inl.intro.intro.e_n
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length (reverse l) < length l
⊢ (length l - 1 - (k + 1) % length (reverse l) + 1) % length l = length l - 1 - k
rw [length_reverse] at *
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k

case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
case H.inl.intro.intro.e_n
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
cases' lt_or_eq_of_le (Nat.succ_le_of_lt hk) with h h
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k

case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
. rw [Nat.mod_eq_of_lt h, ← Nat.sub_add_comm, Nat.succ_sub_succ_eq_sub,
    Nat.mod_eq_of_lt h1]
  exact (Nat.le_sub_iff_add_le (length_pos_of_mem hx)).2 (Nat.succ_le_of_lt h)
no goals
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
. rw [← h]; simp
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ length l - (k + 1) < length l
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ length l - 1 - k < length l
rw [Nat.sub_sub, add_comm]
no goals
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ length l - (k + 1) < length l
exact Nat.sub_lt_self (Nat.succ_pos _) (Nat.succ_le_of_lt (by simpa using hk))
no goals
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
⊢ k < length l
simpa using hk
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ length l - (1 + (k + 1) % length l) < length l
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ length l - 1 - (k + 1) % length (reverse l) < length l
rw [Nat.sub_sub, length_reverse]
no goals
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ length l - (1 + (k + 1) % length l) < length l
exact Nat.sub_lt_self (by rw [add_comm]; exact Nat.succ_pos _)
  (by rw [add_comm]; exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx)))
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 0 < (k + 1) % length l + 1
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 0 < 1 + (k + 1) % length l
rw [add_comm]
no goals
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 0 < (k + 1) % length l + 1
exact Nat.succ_pos _
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ (k + 1) % length l + 1 ≤ length l
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ 1 + (k + 1) % length l ≤ length l
rw [add_comm]
no goals
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
k : ℕ
hk : k < length (reverse l)
hx : nthLe (reverse l) k hk ∈ l
h1 : length l - 1 - k < length l
⊢ (k + 1) % length l + 1 ≤ length l
exact Nat.succ_le_of_lt (Nat.mod_lt _ (length_pos_of_mem hx))
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ Nat.succ k ≤ length l - 1
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
rw [Nat.mod_eq_of_lt h, ← Nat.sub_add_comm, Nat.succ_sub_succ_eq_sub,
  Nat.mod_eq_of_lt h1]
no goals
case H.inl.intro.intro.e_n.inl
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k < length l
⊢ Nat.succ k ≤ length l - 1
exact (Nat.le_sub_iff_add_le (length_pos_of_mem hx)).2 (Nat.succ_le_of_lt h)
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (Nat.succ k - 1 - (k + 1) % Nat.succ k + 1) % Nat.succ k = Nat.succ k - 1 - k
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (length l - 1 - (k + 1) % length l + 1) % length l = length l - 1 - k
rw [← h]
no goals
case H.inl.intro.intro.e_n.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h✝ : Nodup l
k : ℕ
hk✝ : k < length (reverse l)
hk : k < length l
hx : nthLe (reverse l) k hk✝ ∈ l
h1 : length l - 1 - k < length l
h2 : length l - 1 - (k + 1) % length l < length l
h : Nat.succ k = length l
⊢ (Nat.succ k - 1 - (k + 1) % Nat.succ k + 1) % Nat.succ k = Nat.succ k - 1 - k
simp
case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ¬x ∈ reverse l
case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ↑(formPerm l) (↑(formPerm (reverse l)) x) = x
rw [formPerm_apply_of_not_mem x l.reverse, formPerm_apply_of_not_mem _ _ hx]
no goals
case H.inr
α : Type u_1
β : Type ?u.774227
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
x : α
hx : ¬x ∈ l
⊢ ¬x ∈ reverse l
simpa using hx