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