DEFINITION clear_getl_trans()
TYPE =
       ∀i:nat.∀c2:C.∀c3:C.(getl i c2 c3)→∀c1:C.(clear c1 c2)→(getl i c1 c3)
BODY =
Show proof