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