simp only [decide_not, List.mem_singleton_iff, decide_True,
           decide_False, not]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
τ : Type u_1
t : Table ((nm, τ) :: s')
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (decide ¬nm ∈ [nm]) = false
no goals