basic): add a proof that `(a :: l) ≠ l` (#3584)

Commit

5 years ago

feat(data/list/basic): add a proof that `(a :: l) ≠ l` (#3584) `list.cons_ne_self` is motivated by the existence of `nat.succ_ne_self`.

Author

eric-wieser

Parents