lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
qed.
+(* Basic_1: was: pr3_strip *)
+lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 →
+ ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0.
+/3 width=3/ qed.
+
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was pr3_gen_appl *)
theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
/2 width=3/ qed.
+(* Basic_1: was: pr3_flat *)
lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 →
L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
#I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
@(cprs_trans … IHV1) -IHV1 /2 width=1/
qed.
+lemma cprs_abbr: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
+ L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #T1 #T2 #HT12 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_trans … IHV1) -IHV1 /2 width=1/
+qed.
+
(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.