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

Require csuba_defs.
Require csuba_props.
Require csubt_defs.
Require ty3_arity_props.

   Section csubt_arity_props.

      Hints Resolve csuba_arity : ld.

      Lemma csubt_csuba: (g:?; c1,c2:?) (csubt g c1 c2) -> (csuba g c1 c2).
      Proof.
      Intros; XElim H; Clear c1 c2; Intros; XAuto.
(* case 4: csubt_abst *)
      XDecomPoseClear H1 '(ty3_arity ? ? ? ? H1); XDEAuto 3.
      Qed.

   End csubt_arity_props.