+lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2.
+ L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 →
+ ∀a.L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
+#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2
+[ /3 width=1/
+| -HV12 #T #T2 #_ #HT2 #IHT1
+ lapply (cpr_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+ @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/
+]
+qed.
+