-lemma cprs_inv_cast1: â\88\80L,W1,T1,U2. L â\8a¢ â\93£W1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
- â\88\83â\88\83W2,T2. L â\8a¢ W1 â\9e¡* W2 & L â\8a¢ T1 â\9e¡* T2 & U2 = â\93£W2.T2.
+lemma cprs_inv_cast1: â\88\80L,W1,T1,U2. L â\8a¢ â\93\9dW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
+ â\88\83â\88\83W2,T2. L â\8a¢ W1 â\9e¡* W2 & L â\8a¢ T1 â\9e¡* T2 & U2 = â\93\9dW2.T2.