-lemma cprs_inv_cast1 (h) (G) (L): ∀W1,T1,X2. ❪G,L❫ ⊢ ⓝW1.T1 ➡*[h] X2 →
- ∨∨ ∃∃W2,T2. ❪G,L❫ ⊢ W1 ➡*[h] W2 & ❪G,L❫ ⊢ T1 ➡*[h] T2 & X2 = ⓝW2.T2
- | ❪G,L❫ ⊢ T1 ➡*[h] X2.
+lemma cprs_inv_cast1 (h) (G) (L): ∀W1,T1,X2. ❪G,L❫ ⊢ ⓝW1.T1 ➡*[h,0] X2 →
+ ∨∨ ∃∃W2,T2. ❪G,L❫ ⊢ W1 ➡*[h,0] W2 & ❪G,L❫ ⊢ T1 ➡*[h,0] T2 & X2 = ⓝW2.T2
+ | ❪G,L❫ ⊢ T1 ➡*[h,0] X2.