-lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 →
- ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 →
- ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× ⓑ{a,I}V2.T2.
-/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.
-
-lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
- ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶*× T2 & ⇧[d, 1] T ≡ T2.
-#I #G #K #V #T1 elim T1 -T1
-[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
- #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
- destruct
- elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
-| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
- elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
- | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
- ]
-]
+lemma cpy_cpys: ∀G,L,T1,T2,l,m. ⦃G, L⦄ ⊢ T1 ▶[l, m] T2 → ⦃G, L⦄ ⊢ T1 ▶*[l, m] T2.
+/2 width=1 by inj/ qed.
+
+lemma cpys_strap1: ∀G,L,T1,T,T2,l,m.
+ ⦃G, L⦄ ⊢ T1 ▶*[l, m] T → ⦃G, L⦄ ⊢ T ▶[l, m] T2 → ⦃G, L⦄ ⊢ T1 ▶*[l, m] T2.
+normalize /2 width=3 by step/ qed-.
+
+lemma cpys_strap2: ∀G,L,T1,T,T2,l,m.
+ ⦃G, L⦄ ⊢ T1 ▶[l, m] T → ⦃G, L⦄ ⊢ T ▶*[l, m] T2 → ⦃G, L⦄ ⊢ T1 ▶*[l, m] T2.
+normalize /2 width=3 by TC_strap/ qed-.
+
+lemma lsuby_cpys_trans: ∀G,l,m. lsub_trans … (cpys l m G) (lsuby l m).
+/3 width=5 by lsuby_cpy_trans, LTC_lsub_trans/