-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/