no goals
α : Type u_1
β : Type ?u.481863
γ : Type ?u.481866
a : α
s : Finset α
h : ¬a ∈ s
⊢ List.Nodup (a :: toList s)
simp [h, nodup_toList s]
no goals
α : Type u_1
β : Type ?u.481863
γ : Type ?u.481866
a : α
s : Finset α
h : ¬a ∈ s
x : α
⊢ x ∈ toList (cons a s h) ↔ x ∈ a :: toList s
simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]