sta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
| sta_appl: ∀L,V,T,U. sta h L T U →
sta h L (ⓐV.T) (ⓐV.U)
-| sta_cast: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93£W. T) U
+| sta_cast: â\88\80L,W,T,U. sta h L T U â\86\92 sta h L (â\93\9dW. T) U
.
interpretation "static type assignment (term)"
∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
/2 width=3/ qed-.
-fact sta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93£Y.X →
+fact sta_inv_cast1_aux: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢ U â\86\92 â\88\80X,Y. T = â\93\9dY.X →
⦃h, L⦄ ⊢ X • U.
#h #L #T #U * -L -T -U
[ #L #k #X #Y #H destruct
qed.
(* Basic_1: was: sty0_gen_cast *)
-lemma sta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93£Y.X • U → ⦃h, L⦄ ⊢ X • U.
+lemma sta_inv_cast1: â\88\80h,L,X,Y,U. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dY.X • U → ⦃h, L⦄ ⊢ X • U.
/2 width=4/ qed-.