CTS_spec.v
Record
CTS_spec: Type := {
cts_axiom: (relation sort);
cts_rules: sort->sort->sort->Prop;
universes: (relation sort);
head_reduct: Basic_rule
}.
Variable the_CTS: CTS_spec.
(* open the_CTS *)
Local axiom := (cts_axiom the_CTS).
Local rule := (cts_rules the_CTS).
Local univ := (universes the_CTS).
Local hd_rule := (head_reduct the_CTS).
Local hdr := (Rule hd_rule).
Local lifts: (R_lift hdr) := (R_lifts hd_rule).
Local substs: (R_subst hdr) := (R_substs hd_rule).
Local stable: (R_stable_env hdr) := (R_stable hd_rule).
Local red_step := (ctxt hdr).
(* short-cuts *)
Local ctx_stable: (R_stable_env red_step).
Proof (ctxt_stable hdr stable).
Local stable_conv: (R_stable_env (conv hdr)).
Proof (R_rst_stable red_step ctx_stable).
Hints Resolve ctx_stable : pts.
23/12/98, 14:29