no goals
α : Type ?u.667803
β : Type ?u.667806
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ length xs < length (x :: xs)
simp
case h
α : Type u_1
β : Type ?u.667806
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ length xs = length xs
α : Type u_1
β : Type ?u.667806
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) (length xs) (_ : length xs < Nat.succ (length xs))) = x
rw [nthLe_cons_length, formPerm_apply_getLast]
no goals
case h
α : Type u_1
β : Type ?u.667806
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ length xs = length xs
rfl