DEFINITION getl_refl()
TYPE =
       ∀b:B.∀c:C.∀u:T.(getl O (CHead c (Bind b) u) (CHead c (Bind b) u))
BODY =
        assume b: B
        assume c: C
        assume u: T
          (h1) 
             by (drop_refl .)
drop O O (CHead c (Bind b) u) (CHead c (Bind b) u)
          end of h1
          (h2) 
             by (clear_bind . . .)
clear (CHead c (Bind b) u) (CHead c (Bind b) u)
          end of h2
          by (getl_intro . . . . h1 h2)
          we proved getl O (CHead c (Bind b) u) (CHead c (Bind b) u)
       we proved ∀b:B.∀c:C.∀u:T.(getl O (CHead c (Bind b) u) (CHead c (Bind b) u))