(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export lift_defs.

      Inductive cnt: T -> Prop :=
         | cnt_sort: (n:?) (cnt (TSort n))
         | cnt_head: (t:?) (cnt t) -> (k:?; v:?) (cnt (THead k v t)).

      Hint cnt: ld := Constructors cnt.

   Section cnt_props. (******************************************************)

      Lemma cnt_lift: (t:?) (cnt t) ->
                      (i,d:?) (cnt (lift i d t)).
      Proof.
      Intros until 1; XElim H; Clear t; Intros;
      [ Rewrite lift_sort | Rewrite lift_head ]; XAuto.
      Qed.

   End cnt_props.

      Hints Resolve cnt_lift: ld.