+@(cprs_trans … IHV1) -IHV1 /2 width=1/
+qed.
+
+lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2.
+ L.ⓛV ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HV12) -V2
+[ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+| #V0 #V2 #_ #HV02 #IHV01
+ @(cprs_trans … IHV01) -V1 /2 width=2/
+]
+qed.
+
+lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
+ ∀a.L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
+#L #V1 #T1 #T2 #HT12 #V2 #HV12 #a @(cprs_ind … HV12) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_trans … IHV1) -IHV1 /2 width=1/
+qed.
+
+lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
+ ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
+#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
+[ /2 width=1/
+| #T1 #T #HT1 #_ #IHT1
+ lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1
+ @(cprs_trans … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+lemma cprs_abbr2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
+ ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
+#L #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 #a
+lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1
+@(cprs_trans … HV1) -HV1 /2 width=1/
+qed.
+
+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/
+]