no goals
α : Type u_1
β : Type ?u.103482
γ : Type ?u.103485
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
⊢ (insert a s).val = a ::ₘ s.val
rw [insert_val, ndinsert_of_not_mem h]