(****************************************************************************)
(*                                                                          *)
(*                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 clt_defs.

      Fixpoint CTail [k:K; t:T; c:C] : C :=
         Cases c of
            | (CSort n)     => (CHead (CSort n) k t)
            | (CHead d h u) => (CHead (CTail k t d) h u)
         end.

   Section ctail_base_props. (***********************************************)

      Lemma chead_ctail: (c:?; t:?; k:?)
                         (EX h d u | (CHead c k t) = (CTail h u d)).
      Proof.
      XElim c; Intros.
(* case 1: CSort *)
      EApply ex_3_intro with x1:=(CSort n); Simpl; XAuto.
(* case 2: CHead *)
      XDecomPoseClear H '(H t k); Rewrite H0; Clear H0 c k t.
      EApply ex_3_intro with x1:=(CHead x1 k0 t0); Simpl; XAuto.
      Qed.

      Lemma clt_thead: (k:?; u:?; c:?) (clt c (CTail k u c)).
      Proof.
      XElim c; Simpl; XAuto.
      Qed.

      Hints Resolve clt_thead : ld.

      Lemma c_tail_ind: (P:(?->Prop)) ((n:?) (P (CSort n))) ->
                        ((c:?) (P c) -> (k:?; t:?) (P (CTail k t c))) ->
                        (c:?) (P c).
      Proof.
      XElimUsing clt_wf_ind c; XElim c; [ Clear H0 | Clear H ]; Intros.
(* case 1: CSort *)
      XAuto.
(* case 2: CHead *)
      XDecomPose '(chead_ctail c t k); Rewrite H2; Rewrite H2 in H1; XAuto.
      Qed.

   End ctail_base_props.

      Hints Resolve clt_thead : ld.