DEFINITION drop1_gen_pnil()
TYPE =
       ∀c1:C.∀c2:C.(drop1 PNil c1 c2)→(eq C c1 c2)
BODY =
Show proof