theorem notEqByListMem {Attr : Type u_1} {lst : List Attr} {a b : Attr} (a_is_in : a ∈ lst) (b_not_in : ¬b ∈ lst) : a ≠ b