qed-.
lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*[dt, et] U2 →
- â\88\80K,s,d,e. â\87©[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â\87§[d, e] T1 ≡ U1 →
+ â\88\80K,s,d,e. â¬\87[s, d, e] L â\89¡ K â\86\92 â\88\80T1. â¬\86[d, e] T1 ≡ U1 →
d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[d, dt + et - (yinj d + e)] T2 &
- â\87§[d, e] T2 ≡ U2.
+ â¬\86[d, e] T2 ≡ U2.
#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
lapply (cpys_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1
lapply (cpys_weak … HW2 0 (i+1) ? ?) -HW2 //
[ >yplus_O1 >yplus_O1 /3 width=1 by ylt_fwd_le, ylt_inj/ ] -Hi
#HW2 >(cpys_inv_lift1_eq … HW2) -HW2 //
- | elim (ldrop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
+ | elim (drop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
/2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide
#X #_ #H elim (lift_inv_lref2_be … H) -H //