PTS_spec.v

  Variable the_PTS: PTS_sub_spec.

  (* open the PTS *)
  Local axiom := (pts_axiom the_PTS).
  Local rule := (pts_rules the_PTS).
  Local le_type := (Rule (Le_type (pts_le_type the_PTS))).
  Local ge_type := [e:env](transp ? (le_type e)).
  Local le_sort: sort -> sort -> Prop :=
    [s1,s2](e:env)(le_type e (Srt s1) (Srt s2)).
  Hints Unfold le_sort : pts.

  Local le_type_lift: (R_lift le_type).
Proof (R_lifts (Le_type (pts_le_type the_PTS))).

  Local le_type_subst_raw: (R_subst le_type).
Proof (R_substs (Le_type (pts_le_type the_PTS))).

  Local le_type_stable: (R_stable_env le_type).
Proof (R_stable (Le_type (pts_le_type the_PTS))).

  (* short-cuts *)
  Local le_type_refl: (e:env)(t:term)(le_type e t t).
Proof [e:env](preord_refl term (le_type e) (preord (pts_le_type the_PTS) e)).

  Local le_type_trans: (e:env)(x,y,z:term)(le_type e x y)
                                ->(le_type e y z)->(le_type e x z).
Proof [e:env](preord_trans term (le_type e) (preord (pts_le_type the_PTS) e)).

  Hints Resolve le_type_refl : pts.

  Local le_type_subst: (g:env)(d:decl)(x:term)(e:env)(t,u:term)
       (le_type e t u)
     ->(n:nat)(f:env)(sub_in_env g d x n e f)
     ->(le_type f (subst_rec x t n) (subst_rec x u n)).
Intros.
(Cut (R_rt le_type f (subst_rec x t n) (subst_rec x u n)); Intros).
(Elim H1; Intros; Auto with arith pts).
(Apply le_type_trans with y; Auto with arith pts).

(Apply le_type_subst_raw with g:=g d1:=d e:=e; Auto with arith pts).
Save.

  Hints Resolve le_type_lift : pts.

23/12/98, 14:30