Commit 2020-09-28 15:25 50dbce94

fix(data/list/basic): Ensure that ball_cons actually works as a simp lemma (#4281) The LHS of the simp lemma list.ball_cons (aka list.forall_mem_cons) is not in simp-normal form, as list.mem_cons_iff rewrites it. This adds a new simp lemma which is the form that list.mem_cons_iff rewrites it to.