mathlib
50dbce94 - fix(data/list/basic): Ensure that ball_cons actually works as a simp lemma (#4281)

Commit
5 years ago
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.
Author
Parents
Loading