DEFINITION clt_cong()
TYPE =
       ∀c:C.∀d:C.(clt c d)→∀k:K.∀t:T.(clt (CHead c k t) (CHead d k t))
BODY =
Show proof