lemma cpr_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 #T1 #T2 #HT12
lemma cpr_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 #T1 #T2 #HT12