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