INDUCTIVE DEFINITION cnt () [ ]
OF ARITY T→Prop
BUILT FROM:
     cnt_sort: ∀n:nat.(cnt (TSort n))
   | cnt_head: ∀t:T.(cnt t)→∀k:K.∀v:T.(cnt (THead k v t))