DEFINITION getl_mono()
TYPE =
       ∀c:C.∀x1:C.∀h:nat.(getl h c x1)→∀x2:C.(getl h c x2)→(eq C x1 x2)
BODY =
Show proof