mathlib3

51c31cea - refactor(data/list): rm redundant eq_nil_of_forall_not_mem (#804)