X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcpys%2Fcpys_lift.etc;h=59cddfbc9178a6cac9368afb928c42b28ddb3f4e;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=d798c8a627988b5b7af309ac41cd2dc178337101;hpb=e76eade57c0454a58b0d58e5484efe9af417847e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc
index d798c8a62..59cddfbc9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc
@@ -12,165 +12,215 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/substitution/fqus_alt.ma".
-include "basic_2/substitution/cpys.ma".
+include "basic_2/substitution/cpy_lift.ma".
+include "basic_2/multiple/cpys.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
 
-(* Relocation properties ****************************************************)
-
-lemma cpys_lift: ∀G. l_liftable (cpys G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
-  >(lift_mono … H1 … H2) -H1 -H2 //
-| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
-  elim (lift_inv_lref1 … H) * #Hid #H destruct
-  [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
-    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
-    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpys_delta/
-  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
-    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpys_delta/
-  ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
-  elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpys_bind, ldrop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
-  elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpys_flat/
+(* Advanced properties ******************************************************)
+
+lemma cpys_subst: ∀I,G,L,K,V,U1,i,l,m.
+                  l ≤ yinj i → i < l + m →
+                  ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ⫰(l+m-i)] U1 →
+                  ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[l, m] U2.
+#I #G #L #K #V #U1 #i #l #m #Hli #Hilm #HLK #H @(cpys_ind … H) -U1
+[ /3 width=5 by cpy_cpys, cpy_subst/
+| #U #U1 #_ #HU1 #IHU #U2 #HU12
+  elim (lift_total U 0 (i+1)) #U0 #HU0
+  lapply (IHU … HU0) -IHU #H
+  lapply (drop_fwd_drop2 … HLK) -HLK #HLK
+  lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
+  lapply (cpy_weak … HU02 l m ? ?) -HU02
+  [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
+  >yplus_O1 <yplus_inj >ymax_pre_sn_comm /2 width=1 by ylt_fwd_le_succ1/
 ]
 qed.
 
-lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G).
-#G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/
-  ]
-| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
-  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
-  [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
-    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
-    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=9 by cpys_delta, ex2_intro/
-  | elim (le_inv_plus_l … Hid) #Hdie #Hei
-    lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
-    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
-    #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpys_delta, ex2_intro/
+lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,l.
+                     l ≤ yinj i →
+                     ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*[0, ∞] U1 →
+                     ∀U2. ⬆[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*[l, ∞] U2.
+#I #G #L #K #V #U1 #i #l #Hli #HLK #HVU1 #U2 #HU12
+@(cpys_subst … HLK … HU12) >yminus_Y_inj //
+qed.
+
+(* Advanced inversion lemmas *************************************************)
+
+lemma cpys_inv_atom1: ∀I,G,L,T2,l,m. ⦃G, L⦄ ⊢ ⓪{I} ▶*[l, m] T2 →
+                      T2 = ⓪{I} ∨
+                      ∃∃J,K,V1,V2,i. l ≤ yinj i & i < l + m &
+                                    ⬇[i] L ≡ K.ⓑ{J}V1 &
+                                     ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(l+m-i)] V2 &
+                                     ⬆[O, i+1] V2 ≡ T2 &
+                                     I = LRef i.
+#I #G #L #T2 #l #m #H @(cpys_ind … H) -T2
+[ /2 width=1 by or_introl/
+| #T #T2 #_ #HT2 *
+  [ #H destruct
+    elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
+  | * #J #K #V1 #V #i #Hli #Hilm #HLK #HV1 #HVT #HI
+    lapply (drop_fwd_drop2 … HLK) #H
+    elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
+    [2,3,4: /2 width=1 by ylt_fwd_le_succ1, yle_succ_dx/ ]
+    /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
   ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5 by cpys_bind, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1
-  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpys_flat, lift_flat, ex2_intro/
 ]
 qed-.
 
-(* Properties on supclosure *************************************************)
-
-lemma fqu_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                      ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
-                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 
-/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpys_pair_sn, cpys_bind, cpys_flat, ex2_intro/
-[ #I #G #L #V2 #U2 #HVU2
-  elim (lift_total U2 0 1)
-  /4 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
-| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
-  elim (lift_total T2 0 (e+1))
-  /3 width=11 by cpys_lift, fqu_drop, ex2_intro/
+lemma cpys_inv_lref1: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 →
+                      T2 = #i ∨
+                      ∃∃I,K,V1,V2. l ≤ i & i < l + m &
+                                   ⬇[i] L ≡ K.ⓑ{I}V1 &
+                                   ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(l+m-i)] V2 &
+                                   ⬆[O, i+1] V2 ≡ T2.
+#G #L #T2 #i #l #m #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
+* #I #K #V1 #V2 #j #Hlj #Hjlm #HLK #HV12 #HVT2 #H destruct /3 width=7 by ex5_4_intro, or_intror/
+qed-.
+
+lemma cpys_inv_lref1_Y2: ∀G,L,T2,i,l. ⦃G, L⦄ ⊢ #i ▶*[l, ∞] T2 →
+                         T2 = #i ∨
+                         ∃∃I,K,V1,V2. l ≤ i & ⬇[i] L ≡ K.ⓑ{I}V1 &
+                                      ⦃G, K⦄ ⊢ V1 ▶*[0, ∞] V2 & ⬆[O, i+1] V2 ≡ T2.
+#G #L #T2 #i #l #H elim (cpys_inv_lref1 … H) -H /2 width=1 by or_introl/
+* >yminus_Y_inj /3 width=7 by or_intror, ex4_4_intro/
+qed-.
+
+lemma cpys_inv_lref1_drop: ∀G,L,T2,i,l,m. ⦃G, L⦄ ⊢ #i ▶*[l, m] T2 →
+                            ∀I,K,V1. ⬇[i] L ≡ K.ⓑ{I}V1 →
+                            ∀V2. ⬆[O, i+1] V2 ≡ T2 →
+                            ∧∧ ⦃G, K⦄ ⊢ V1 ▶*[0, ⫰(l+m-i)] V2
+                             & l ≤ i
+                             & i < l + m.
+#G #L #T2 #i #l #m #H #I #K #V1 #HLK #V2 #HVT2 elim (cpys_inv_lref1 … H) -H
+[ #H destruct elim (lift_inv_lref2_be … HVT2) -HVT2 -HLK /2 width=1 by ylt_inj/
+| * #Z #Y #X1 #X2 #Hli #Hilm #HLY #HX12 #HXT2
+  lapply (lift_inj … HXT2 … HVT2) -T2 #H destruct
+  lapply (drop_mono … HLY … HLK) -L #H destruct
+  /2 width=1 by and3_intro/
 ]
 qed-.
 
-lemma fquq_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_cpys_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
-| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+(* Properties on relocation *************************************************)
+
+lemma cpys_lift_le: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
+                    ∀L,U1,s,l,m. lt + mt ≤ l → ⬇[s, l, m] L ≡ K →
+                    ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
+                    ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2.
+#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hlmtl #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T l m) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 ]
 qed-.
 
-lemma fqup_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpys_trans … H12 … HTU2) -T2
-  /3 width=3 by fqu_fqup, ex2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
-  elim (fqu_cpys_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
-  elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/
+lemma cpys_lift_be: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
+                    ∀L,U1,s,l,m. lt ≤ l → l ≤ lt + mt →
+                    ⬇[s, l, m] L ≡ K → ⬆[l, m] T1 ≡ U1 →
+                    ∀U2. ⬆[l, m] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*[lt, mt + m] U2.
+#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hltl #Hllmt #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T l m) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 ]
 qed-.
 
-lemma fqus_cpys_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                       ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 →
-                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H
-[ #HT12 elim (fqup_cpys_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
-| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+lemma cpys_lift_ge: ∀G,K,T1,T2,lt,mt. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 →
+                    ∀L,U1,s,l,m. l ≤ lt → ⬇[s, l, m] L ≡ K →
+                    ⬆[l, m] T1 ≡ U1 → ∀U2. ⬆[l, m] T2 ≡ U2 →
+                    ⦃G, L⦄ ⊢ U1 ▶*[lt+m, mt] U2.
+#G #K #T1 #T2 #lt #mt #H #L #U1 #s #l #m #Hllt #HLK #HTU1 @(cpys_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T l m) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (cpy_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 /2 width=3 by cpys_strap1/
 ]
 qed-.
 
-lemma fqu_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
-                          ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
-  #U2 #HVU2 @(ex3_intro … U2)
-  [1,3: /3 width=7 by fqu_drop, cpys_delta, ldrop_pair, ldrop_ldrop/
-  | #H destruct /2 width=7 by lift_inv_lref2_be/
-  ]
-| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
-  [1,3: /2 width=4 by fqu_pair_sn, cpys_pair_sn/
-  | #H0 destruct /2 width=1 by/
-  ]
-| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2))
-  [1,3: /2 width=4 by fqu_bind_dx, cpys_bind/
-  | #H0 destruct /2 width=1 by/
-  ]
-| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2))
-  [1,3: /2 width=4 by fqu_flat_dx, cpys_flat/
-  | #H0 destruct /2 width=1 by/
-  ]
-| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
-  #U2 #HTU2 @(ex3_intro … U2)
-  [1,3: /2 width=9 by cpys_lift, fqu_drop/
-  | #H0 destruct /3 width=5 by lift_inj/
+(* Inversion lemmas for relocation ******************************************)
+
+lemma cpys_inv_lift1_le: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                         ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                         lt + mt ≤ l →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt] T2 & ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmtl @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_be: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                         ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                         lt ≤ l → l + m ≤ lt + mt →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, mt - m] T2 & ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmlmt @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                         ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                         l + m ≤ lt →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt - m, mt] T2 & ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hlmlt @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas on relocation **********************************)
+
+lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                            ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                            l ≤ lt → lt ≤ l + m → l + m ≤ lt + mt →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[l, lt + mt - (l + m)] T2 &
+                                 ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hllt #Hltlm #Hlmlmt @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 ]
 qed-.
 
-lemma fquq_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
-                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
-                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
-[ #H12 elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
-  /3 width=4 by fqu_fquq, ex3_intro/
-| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
+lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                            ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                            lt ≤ l → lt + mt ≤ l + m →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hlmtlm @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 ]
 qed-.
 
-lemma fqup_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
-                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
-                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
-[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpys_trans_neq … H12 … HTU2 H) -T2
-  /3 width=4 by fqu_fqup, ex3_intro/
-| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
-  #U1 #HTU1 #H #H12 elim (fqu_cpys_trans_neq … H1 … HTU1 H) -T1
-  /3 width=8 by fqup_strap2, ex3_intro/
+lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,lt,mt. ⦃G, L⦄ ⊢ U1 ▶*[lt, mt] U2 →
+                            ∀K,s,l,m. ⬇[s, l, m] L ≡ K → ∀T1. ⬆[l, m] T1 ≡ U1 →
+                            lt ≤ l → l ≤ lt + mt → lt + mt ≤ l + m →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*[lt, l - lt] T2 & ⬆[l, m] T2 ≡ U2.
+#G #L #U1 #U2 #lt #mt #H #K #s #l #m #HLK #T1 #HTU1 #Hltl #Hllmt #Hlmtlm @(cpys_ind … H) -U2
+[ /2 width=3 by ex2_intro/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
 ]
 qed-.
 
-lemma fqus_cpys_trans_neq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
-                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ▶*× U2 → (T2 = U2 → ⊥) →
-                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ▶*× U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
-[ #H12 elim (fqup_cpys_trans_neq … H12 … HTU2 H) -T2
-  /3 width=4 by fqup_fqus, ex3_intro/
-| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
+lemma cpys_inv_lift1_subst: ∀G,L,W1,W2,l,m. ⦃G, L⦄ ⊢ W1 ▶*[l, m] W2 →
+                            ∀K,V1,i. ⬇[i+1] L ≡ K → ⬆[O, i+1] V1 ≡ W1 →
+                            l ≤ yinj i → i < l + m →
+                            ∃∃V2.  ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(l+m-i)] V2 & ⬆[O, i+1] V2 ≡ W2.
+#G #L #W1 #W2 #l #m #HW12 #K #V1 #i #HLK #HVW1 #Hli #Hilm
+elim (cpys_inv_lift1_ge_up … HW12 … HLK … HVW1 ? ? ?) //
+>yplus_O1 <yplus_inj >yplus_SO2
+[ >yminus_succ2 /2 width=3 by ex2_intro/
+| /2 width=1 by ylt_fwd_le_succ1/
+| /2 width=3 by yle_trans/
 ]
 qed-.