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