]
qed-.
-lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93£W. T ➡* U →
- â\93£W. T ≃ U ∨ L ⊢ T ➡* U.
+lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93\9dW. T ➡* U →
+ â\93\9dW. T ≃ U ∨ L ⊢ T ➡* U.
#L #W #T #U #H
elim (cprs_inv_cast1 … H) -H /2 width=1/ *
#W0 #T0 #_ #_ #H destruct /2 width=1/