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 =
        assume c: C
        assume d: C
          we must prove (clt c d)→∀k:K.∀t:T.(clt (CHead c k t) (CHead d k t))
          or equivalently 
                lt (cweight c) (cweight d)
                  →K→∀t:T.(clt (CHead c __2 t) (CHead d __2 t))
           suppose H: lt (cweight c) (cweight d)
           assume : K
           assume t: T
             by (lt_reg_r . . . H)
             we proved 
                lt
                  plus (cweight c) (tweight t)
                  plus (cweight d) (tweight t)
             that is equivalent to clt (CHead c __2 t) (CHead d __2 t)
          we proved 
             lt (cweight c) (cweight d)
               →K→∀t:T.(clt (CHead c __2 t) (CHead d __2 t))
          that is equivalent to (clt c d)→∀k:K.∀t:T.(clt (CHead c k t) (CHead d k t))
       we proved ∀c:C.∀d:C.(clt c d)→∀k:K.∀t:T.(clt (CHead c k t) (CHead d k t))