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

      Fixpoint cbk [c:C] : nat := Cases c of
         | (CSort m)     => m
         | (CHead c _ _) => (cbk c)
      end.

      Fixpoint app1 [c:C] : T -> T := [t:?] Cases c of
         | (CSort _)     => t
         | (CHead c k u) => (app1 c (THead k u t))
      end.