+lemma cpcs_beta_dx: ∀L,V1,V2,W,T1,T2.
+ L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛW.T1 ⬌* ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 #HV12 #HT12
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+lapply (cprs_beta_dx … HV12 HT1) -HV12 -HT1 #HT1
+lapply (cprs_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+@(cprs_div … HT1) /2 width=1/
+qed.
+
+lemma cpcs_beta_dx_tpr_rev: ∀L,V1,V2,W,T1,T2.
+ V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 →
+ L ⊢ ⓓV2.T2 ⬌* ⓐV1.ⓛW.T1.
+/4 width=1/ qed.
+