qed-.
(* Basic_1: was: pr3_iso_appls_cast *)
-lemma cprs_fwd_tau_vector: â\88\80L,Vs,W,T,U. L â\8a¢ â\92¶Vs. â\93£W. T ➡* U →
- â\92¶Vs. â\93£W. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
+lemma cprs_fwd_tau_vector: â\88\80L,Vs,W,T,U. L â\8a¢ â\92¶Vs. â\93\9dW. T ➡* U →
+ â\92¶Vs. â\93\9dW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/
#V #Vs #IHVs #W #T #U #H
elim (cprs_inv_appl1 … H) -H *