(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
definition nta (a) (h): relation4 genv lenv term term ≝
- λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+ λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
interpretation "native type assignment (term)"
'Colon a h G L T U = (nta a h G L T U).
interpretation "restricted native type assignment (term)"
- 'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
+ 'Colon h G L T U = (nta (ac_eq (S O)) h G L T U).
interpretation "extended native type assignment (term)"
- 'ColonStar h G L T U = (nta Y h G L T U).
+ 'ColonStar h G L T U = (nta ac_top h G L T U).
(* Basic properties *********************************************************)
(* Basic_forward lemmas *****************************************************)
lemma nta_fwd_cnv_sn (a) (h) (G) (L):
- ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
#a #h #G #L #T #U #H
elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
qed-.
(* Note: this is nta_fwd_correct_cnv *)
lemma nta_fwd_cnv_dx (a) (h) (G) (L):
- ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
#a #h #G #L #T #U #H
elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
qed-.