basic): `λ a, [a]` is injective (#16716)

Commit

3 years ago

feat(data/list/basic): `λ a, [a]` is injective (#16716) Also add a `@[simp]` lemma `list.cons_eq_cons`

Author

urkud

Parents