DEFINITION clear_trans()
TYPE =
       ∀c1:C.∀c:C.(clear c1 c)→∀c2:C.(clear c c2)→(clear c1 c2)
BODY =
Show proof