### 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