DEFINITION getl_gen_O()
TYPE =
∀
e:
C
.
∀
x:
C
.(
getl
O
e x)
→
(
clear
e x)
BODY =
Show proof