-lemma cpr_abbr_pos (h) (o) (G) (L) (V) (T1):
- ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛[h, o] T2 → ⊥).
-#h #o #G #L #V #U1
+lemma cpr_abbr_pos (h) (G) (L) (V) (T1):
+ ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛ T2 → ⊥).
+#h #G #L #V #U1
[ elim (tdeq_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
/3 width=9 by cpm_zeta, tdeq_lifts_inv_pair_sn, ex2_intro/
| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H
[ elim (tdeq_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
/3 width=9 by cpm_zeta, tdeq_lifts_inv_pair_sn, ex2_intro/
| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H