DEFINITION cnt_lift()
TYPE =
       ∀t:T.(cnt t)→∀i:nat.∀d:nat.(cnt (lift i d t))
BODY =
Show proof