DEFINITION drop_mono()
TYPE =
       ∀c:C.∀x1:C.∀d:nat.∀h:nat.(drop h d c x1)→∀x2:C.(drop h d c x2)→(eq C x1 x2)
BODY =
Show proof