DEFINITION csuba_clear_trans()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(csuba g c2 c1)→∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c2 e2)
BODY =
Show proof