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