agda/agda-stdlib — pull request #22 by pepijnkokke (2014-06-19 11:03:28+00:00)
Title: Adding drop-length and take-length.

Added two simple but useful properties stating that dropping or taking with the length results in the empty/input list, respectively.