DEFINITION getl_refl()
TYPE =
       ∀b:B.∀c:C.∀u:T.(getl O (CHead c (Bind b) u) (CHead c (Bind b) u))
BODY =
Show proof