nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93£U. T) U
+| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93\9dU. T) U
| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
nta h L T U2
.
(* Basic_1: was: ty3_cast *)
lemma nta_cast_old: ∀h,L,W,T,U.
- â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : â\93£W.U.
+ â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : â\93\9dW.U.
/4 width=3/ qed.
(* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : T0.
+lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : T0.
/3 width=2/ qed.
-(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
+(* Basic_1: removed theorems 4:
+ ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
+*)