PLFA agda exercises
open import TakeDropDec