(* Properties on context-sensitive parallel equivalence for terms ***********)
-lemma lsubsv_cpcs_trans: â\88\80h,g,G,L1,L2. G â\8a¢ L1 ¡â\8a\91[h, g] L2 →
+lemma lsubsv_cpcs_trans: â\88\80h,g,G,L1,L2. G â\8a¢ L1 ¡â«\83[h, g] L2 →
∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
/3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
qed-.