ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
| ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W →
ntaa h L (ⓐV.T) (ⓐV.U)
-| ntaa_cast: â\88\80L,T,U,W. ntaa h L T U â\86\92 ntaa h L U W â\86\92 ntaa h L (â\93£U. T) U
+| ntaa_cast: â\88\80L,T,U,W. ntaa h L T U â\86\92 ntaa h L U W â\86\92 ntaa h L (â\93\9dU. T) U
| ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 →
ntaa h L T U2
.
) →
(∀L,T,U,W.
⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
- R L T U â\86\92 R L U W â\86\92 R L (â\93£U.T) U
+ R L T U â\86\92 R L U W â\86\92 R L (â\93\9dU.T) U
) →
(∀L,T,U1,U2,V2.
⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →