type binder_type =
   Declaration
 | Definition
;;

type context = (binder_type * Cic.name * Cic.term) list;;

type sequent = context * Cic.term;;