-lemma cpr_inv_flat1: â\88\80h,I,G,L,V1,U1,U2. â¦\83G,Lâ¦\84 â\8a¢ â\93\95{I}V1.U1 ➡[h] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G,Lâ¦\84 ⊢ U1 ➡[h] T2 &
- U2 = ⓕ{I}V2.T2
- | (â¦\83G,Lâ¦\84 ⊢ U1 ➡[h] U2 ∧ I = Cast)
- | â\88\83â\88\83p,V2,W1,W2,T1,T2. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡[h] V2 & â¦\83G,Lâ¦\84 ⊢ W1 ➡[h] W2 &
- â¦\83G,L.â\93\9bW1â¦\84 â\8a¢ T1 â\9e¡[h] T2 & U1 = â\93\9b{p}W1.T1 &
- U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
- | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â¦\83G,Lâ¦\84 ⊢ V1 ➡[h] V & ⇧*[1] V ≘ V2 &
- â¦\83G,Lâ¦\84 â\8a¢ W1 â\9e¡[h] W2 & â¦\83G,L.â\93\93W1â¦\84 ⊢ T1 ➡[h] T2 &
- U1 = ⓓ{p}W1.T1 &
- U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
+lemma cpr_inv_flat1: â\88\80h,I,G,L,V1,U1,U2. â\9dªG,Lâ\9d« â\8a¢ â\93\95[I]V1.U1 ➡[h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡[h] V2 & â\9dªG,Lâ\9d« ⊢ U1 ➡[h] T2 &
+ U2 = ⓕ[I]V2.T2
+ | (â\9dªG,Lâ\9d« ⊢ U1 ➡[h] U2 ∧ I = Cast)
+ | â\88\83â\88\83p,V2,W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡[h] V2 & â\9dªG,Lâ\9d« ⊢ W1 ➡[h] W2 &
+ â\9dªG,L.â\93\9bW1â\9d« â\8a¢ T1 â\9e¡[h] T2 & U1 = â\93\9b[p]W1.T1 &
+ U2 = ⓓ[p]ⓝW2.V2.T2 & I = Appl
+ | â\88\83â\88\83p,V,V2,W1,W2,T1,T2. â\9dªG,Lâ\9d« ⊢ V1 ➡[h] V & ⇧*[1] V ≘ V2 &
+ â\9dªG,Lâ\9d« â\8a¢ W1 â\9e¡[h] W2 & â\9dªG,L.â\93\93W1â\9d« ⊢ T1 ➡[h] T2 &
+ U1 = ⓓ[p]W1.T1 &
+ U2 = ⓓ[p]W2.ⓐV2.T2 & I = Appl.