basic): `list.head`, `list.head'`, and `list.tail` are surjective (#16625)

Commit

3 years ago

feat(data/list/basic): `list.head`, `list.head'`, and `list.tail` are surjective (#16625) Also add `list.eq_cons_of_mem_head'`, a more specific version of `list.mem_of_mem_head'`

Author

urkud

Parents

19deedcc

mathlib3 a48b8eff - feat(data/list/basic): `list.head`, `list.head'`, and `list.tail` are surjective (#16625)

mathlib3
a48b8eff - feat(data/list/basic): `list.head`, `list.head'`, and `list.tail` are surjective (#16625)