α : Type u_1
β : Type ?u.1320
n : ℕ
a a' : α
⊢ ¬a ∈ toList { val := [], property := (_ : List.length [] = List.length []) }
α : Type u_1
β : Type ?u.1320
n : ℕ
a a' : α
⊢ ¬a ∈ toList nil
unfold Vector.nil
α : Type u_1
β : Type ?u.1320
n : ℕ
a a' : α
⊢ ¬a ∈ []
α : Type u_1
β : Type ?u.1320
n : ℕ
a a' : α
⊢ ¬a ∈ toList { val := [], property := (_ : List.length [] = List.length []) }
dsimp
no goals
α : Type u_1
β : Type ?u.1320
n : ℕ
a a' : α
⊢ ¬a ∈ []
simp