-lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
- ∀i. d ≤ yinj i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
+lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,l,m. ⦃G, L⦄ ⊢ U1 ▶[l, m] U2 →
+ ∀i. l ≤ yinj i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
- ∃∃I,K,W,j. d ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W &
+ ∃∃I,K,W,j. l ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W &
[ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
[ /4 width=9 by nlift_bind_sn, or_introl/
| * /5 width=9 by nlift_bind_sn, ex5_4_intro, or_intror/
]
| #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
[ /4 width=9 by nlift_bind_dx, or_introl/
[ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
[ /4 width=9 by nlift_bind_sn, or_introl/
| * /5 width=9 by nlift_bind_sn, ex5_4_intro, or_intror/
]
| #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
[ /4 width=9 by nlift_bind_dx, or_introl/
lapply (ylt_O … Hj) -Hj #Hj
lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK
>(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
lapply (ylt_O … Hj) -Hj #Hj
lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK
>(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
/5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/
]
]
/5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/
]
]
[ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
[ /4 width=9 by nlift_flat_sn, or_introl/
| * /5 width=9 by nlift_flat_sn, ex5_4_intro, or_intror/
[ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
[ /4 width=9 by nlift_flat_sn, or_introl/
| * /5 width=9 by nlift_flat_sn, ex5_4_intro, or_intror/