DEFINITION drop_gen_refl()
TYPE =
∀
x:
C
.
∀
e:
C
.(
drop
O
O
x e)
→
(
eq
C
x e)
BODY =
Show proof