#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
[ //
| #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
- elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
| /4 width=1 by lsuby_succ, cpy_bind/
| /3 width=1 by cpy_flat/
]
]
qed-.
+(* Note: lemma 1250 *)
lemma cpy_weak_top: ∀G,L,T1,T2,d,e.
⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2.
#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e //