From a92f724a46a78af74121c44bbb06c4ec51f9555e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 23 Mar 2021 12:19:30 +0000
Subject: Replace transfer with shift.

Prove substitution in the unguarded context.
---
 src/Cfe/Context/Properties.agda | 224 +++++++++++++++++++++++-----------------
 1 file changed, 130 insertions(+), 94 deletions(-)

(limited to 'src/Cfe/Context/Properties.agda')

diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index 230c18b..11441a7 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid; Symmetric)
+open import Relation.Binary using (Setoid; Symmetric; Transitive)
 
 module Cfe.Context.Properties
   {c ℓ} (over : Setoid c ℓ)
@@ -20,102 +20,138 @@ open import Relation.Binary.PropositionalEquality
 ≋-sym : ∀ {n} → Symmetric (_≋_ {n})
 ≋-sym (refl , refl , refl) = refl , refl , refl
 
-cast-involutive : ∀ {a A k m n} .(k≡m : k ≡ m) .(m≡n : m ≡ n) .(k≡n : _) xs → C.cast m≡n (C.cast {a} {A} k≡m xs) ≡ C.cast k≡n xs
-cast-involutive {k = zero} {zero} {zero} k≡m m≡n k≡n [] = refl
-cast-involutive {k = suc _} {suc _} {suc _} k≡m m≡n k≡n (x ∷ xs) = cong (x ∷_) (cast-involutive (cong ℕ.pred k≡m) (cong ℕ.pred m≡n) (cong ℕ.pred k≡n) xs)
+≋-trans : ∀ {n} → Transitive (_≋_ {n})
+≋-trans (refl , refl , refl) (refl , refl , refl) = refl , refl , refl
 
-cast-insert : ∀ {a A m n} xs .(m≡n : _) i j .(_ : toℕ i ≡ toℕ j) y → C.cast {a} {A} {suc m} {suc n} (cong suc m≡n) (insert xs i y) ≡ insert (C.cast m≡n xs) j y
-cast-insert [] m≡n zero zero _ y = refl
-cast-insert (x ∷ xs) m≡n zero zero _ y = refl
-cast-insert {m = suc _} {n = suc _} (x ∷ xs) m≡n (suc i) (suc j) i≡j y = cong (x ∷_) (cast-insert xs (cong ℕ.pred m≡n) i j (cong ℕ.pred i≡j) y)
-
-wkn₁-shift : ∀ {n} (Γ,Δ : Context n) i i≥m τ → shift (wkn₁ Γ,Δ i i≥m τ) ≋ wkn₁ (shift Γ,Δ) i z≤n τ
-wkn₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≥m τ =
-  refl ,
-  eq Δ Γ m≤n i i≥m τ ,
-  refl
+shift≤-wkn₁-comm : ∀ {n i j} Γ,Δ i≤m j≥m τ →
+                   shift≤ {i = i} (wkn₁ {n} {j} Γ,Δ j≥m τ) i≤m ≋
+                   wkn₁ (shift≤ Γ,Δ i≤m) (≤-trans i≤m j≥m) τ
+shift≤-wkn₁-comm record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤m j≥m τ =
+  refl , eq Γ Δ m≤n i≤m j≥m τ , refl
   where
-  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i (i≥m : toℕ i ≥ m) y →
-       C.cast {a} {A}
-         (trans (sym (+-∸-assoc m (≤-step m≤n))) (m+n∸m≡n m (suc n)))
-         (xs ++ C.cast (sym (+-∸-assoc 1 m≤n)) (insert ys (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) y)) ≡
-       C.cast refl (insert (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (xs ++ ys)) (F.cast refl i) y)
-  eq [] [] m≤n zero i≥m y = refl
-  eq [] (x ∷ ys) m≤n zero i≥m y = refl
-  eq [] (x ∷ ys) m≤n (suc i) i≥m y = cong (x ∷_) (eq [] ys z≤n i z≤n y)
-  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n (suc i) (s≤s i≥m) y = cong (x ∷_) (eq xs ys (pred-mono m≤n) i i≥m y)
-
-wkn₂-shift : ∀ {n} (Γ,Δ : Context n) i i≤m τ → shift (wkn₂ Γ,Δ i i≤m τ) ≋ wkn₁ (shift Γ,Δ) i z≤n τ
-wkn₂-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≤m τ =
-  refl ,
-  eq Δ Γ m≤n i i≤m τ ,
-  refl
+  eq : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤m : i ℕ.≤ m) (j≥m : toℕ {suc n} j ≥ m) y →
+       drop′ {a} {A} (≤-step m≤n) i≤m (ys ++ (insert′ xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) j≥m) y)) ≡
+       insert′ (drop′ m≤n i≤m (ys ++ xs)) (s≤s (≤-trans i≤m m≤n)) (reduce≥′ (≤-step (≤-trans i≤m m≤n)) (≤-trans i≤m j≥m)) y
+  eq _ [] z≤n z≤n _ _ = refl
+  eq {j = suc _} xs (x ∷ ys) (s≤s m≤n) z≤n (s≤s j≥m) y = cong (x ∷_) (eq xs ys m≤n z≤n j≥m y)
+  eq {j = suc _} xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤m) (s≤s j≥m) y = eq xs ys m≤n i≤m j≥m y
+
+shift≤-wkn₂-comm-≤ : ∀ {n i j} Γ,Δ i≤j j≤m τ →
+                     shift≤ {i = i} (wkn₂ {n} {j} Γ,Δ j≤m τ) (≤-trans i≤j (≤-step j≤m)) ≋
+                     wkn₁ (shift≤ Γ,Δ (≤-trans i≤j j≤m)) i≤j τ
+shift≤-wkn₂-comm-≤ record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m τ =
+  refl , eq₁ Γ Δ m≤n i≤j j≤m τ , eq₂ Δ i≤j j≤m τ
   where
-  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i (i≤m : toℕ i ℕ.≤ m) y →
-       C.cast {a} {A}
-         (trans (sym (+-∸-assoc (suc m) (s≤s m≤n))) (m+n∸m≡n (suc m) (suc n)))
-         (insert xs (fromℕ< (s≤s i≤m)) y ++ ys) ≡
-       C.cast
-         (sym (+-∸-assoc 1 z≤n))
-         (insert (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (xs ++ ys))
-                 (F.cast (+-∸-assoc 1 z≤n) (reduce≥′ (≤-step z≤n) i z≤n)) y)
-  eq [] [] m≤n zero i≤m y = refl
-  eq [] (x ∷ ys) m≤n zero i≤m y = cong (λ z → y ∷ x ∷ z) (sym (cast-involutive refl refl refl ys))
-  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n zero i≤m y =
-    cong (λ z → y ∷ x ∷ z)
-         (sym (cast-involutive (trans (sym (+-∸-assoc m (pred-mono m≤n))) (m+n∸m≡n m n))
-                               refl
-                               (trans (sym (+-∸-assoc m (pred-mono m≤n))) (m+n∸m≡n m n))
-                               (xs ++ ys)))
-  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n (suc i) (s≤s i≤m) y = cong (x ∷_) (eq xs ys (pred-mono m≤n) i i≤m y)
-
-rotate₁-shift : ∀ {n} (Γ,Δ : Context n) i j i≥m i≤j → rotate₁ (shift Γ,Δ) i j z≤n i≤j ≋ shift (rotate₁ Γ,Δ i j i≥m i≤j)
-rotate₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i≥m i≤j =
-  refl ,
-  eq Γ Δ m≤n i j i≥m i≤j ,
-  refl
+  eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : i ℕ.≤ toℕ {suc n} j) (j≤m : toℕ j ℕ.≤ m) y →
+        drop′ {a} {A} (s≤s m≤n) (≤-trans i≤j (≤-step j≤m)) (insert ys (fromℕ< (s≤s j≤m)) y ++ xs) ≡
+        insert′
+          (drop′ m≤n (≤-trans i≤j j≤m) (ys ++ xs))
+          (s≤s (≤-trans (≤-trans i≤j j≤m) m≤n))
+          (reduce≥′ (≤-step (≤-trans (≤-trans i≤j j≤m) m≤n)) i≤j)
+          y
+  eq₁ {j = zero} _ _ _ z≤n _ _ = refl
+  eq₁ {j = suc j} xs (x ∷ ys) (s≤s m≤n) z≤n (s≤s j≤m) y = cong (x ∷_) (eq₁ xs ys m≤n z≤n j≤m y)
+  eq₁ {j = suc j} xs (x ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = eq₁ xs ys m≤n i≤j j≤m y
+
+  eq₂ : ∀ {a A n m i j} ys (i≤j : i ℕ.≤ toℕ {suc n} j) (j≤m : toℕ j ℕ.≤ m) y →
+        take′ {a} {A} (≤-trans i≤j (≤-step j≤m)) (insert ys (fromℕ< (s≤s j≤m)) y) ≡
+        take′ (≤-trans i≤j j≤m) ys
+  eq₂ {j = zero} _ z≤n _ _ = refl
+  eq₂ {j = suc _} _ z≤n _ _ = refl
+  eq₂ {j = suc zero} (_ ∷ _) (s≤s z≤n) (s≤s _) _ = refl
+  eq₂ {j = suc (suc _)} (x ∷ ys) (s≤s i≤j) (s≤s j≤m) y = cong (x ∷_) (eq₂ ys i≤j j≤m y)
+
+shift≤-wkn₂-comm-> : ∀ {n i j} Γ,Δ i≤j j≤m τ →
+                     shift≤ {i = suc j} (wkn₂ {n} {i} Γ,Δ (≤-trans i≤j j≤m) τ) (s≤s j≤m) ≋
+                     wkn₂ (shift≤ Γ,Δ j≤m) i≤j τ
+shift≤-wkn₂-comm-> record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m τ = refl , eq₁ Γ Δ m≤n i≤j j≤m τ , eq₂ Δ m≤n i≤j j≤m τ
   where
-  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i j i≥m i≤j →
-    rotate {a} {A} i j i≤j (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ xs)) ≡
-    C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ rotate (reduce≥′ m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs)
-  eq {m = zero} {suc _} (x ∷ xs) [] _ zero j _ _ = sym (cast-insert xs refl j j refl x)
-  eq {m = zero} (x ∷ xs) [] _ (suc i) (suc j) _ i≤j = cong (x ∷_) (eq xs [] z≤n i j z≤n (pred-mono i≤j))
-  eq {m = suc _} {suc _} xs (y ∷ ys) m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = cong (y ∷_) (eq xs ys (pred-mono m≤n) i j i≥m i≤j)
-
-transfer-cons : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m τ → transfer (cons Γ,Δ τ) (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m) ≋ cons (transfer Γ,Δ i j i<m 1+j≥m) τ
-transfer-cons record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m τ =
-  refl , eq₁ Γ Δ m≤n (fromℕ< i<m) j 1+j≥m τ , eq₂ Δ (fromℕ< i<m) τ
+  eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : toℕ {suc n} i ℕ.≤ j) (j≤m : j ℕ.≤ m) y →
+        drop′ {a} {A} (s≤s m≤n) (s≤s j≤m) (insert ys (fromℕ< (s≤s (≤-trans i≤j j≤m))) y ++ xs) ≡
+        drop′ m≤n j≤m (ys ++ xs)
+  eq₁ {i = zero} _ _ _ _ _ _ = refl
+  eq₁ {i = suc _} xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = eq₁ xs ys m≤n i≤j j≤m y
+
+  eq₂ : ∀ {a A n m i j} ys (m≤n : m ℕ.≤ n) (i≤j : toℕ {suc n} i ℕ.≤ j) (j≤m : j ℕ.≤ m) y →
+        take′ {a} {A} (s≤s j≤m) (insert ys (fromℕ< (s≤s (≤-trans i≤j j≤m))) y) ≡
+        insert (take′ j≤m ys) (fromℕ< (s≤s i≤j)) y
+  eq₂ {i = zero} _ _ _ _ _ = refl
+  eq₂ {i = suc _} (x ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = cong (x ∷_) (eq₂ ys m≤n i≤j j≤m y)
+
+shift≤-identity : ∀ {n} Γ,Δ → shift≤ {n} Γ,Δ ≤-refl ≋ Γ,Δ
+shift≤-identity record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } = refl , eq₁ Γ Δ m≤n , eq₂ Δ
   where
-  eq₁ : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) (i : Fin (suc m)) j .(1+j≥m : _) y →
-    insert′ {a} {A} xs (s≤s m≤n) (λ ()) (reduce≥′ (≤-step m≤n) (suc j) 1+j≥m) (lookup (y ∷ ys) (suc i)) ≡
-    insert′ xs m≤n (λ ()) (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) (lookup ys i)
-  eq₁ {m = zero} {suc _} xs ys m≤n i j 1+j≥m y = refl
-  eq₁ {m = suc m} xs ys m≤n i zero 1+j≥m x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
-  eq₁ {m = suc m} {suc _} xs (x ∷ ys) m≤n i (suc j) 1+j≥m y = refl
-
-  eq₂ : ∀ {a A m} ys (i : Fin (suc m)) y →
-    remove′ {a} {A} (y ∷ ys) (λ ()) (suc i) ≡ y ∷ remove′ ys (λ ()) i
-  eq₂ (x ∷ ys) i y = refl
-
-transfer-shift : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m → rotate₁ (shift Γ,Δ) i j z≤n (pred-mono (≤-trans i<m 1+j≥m)) ≋ shift (transfer Γ,Δ i j i<m 1+j≥m)
-transfer-shift record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m =
-  refl ,
-  eq Γ Δ m≤n i j i<m 1+j≥m ,
-  refl
+  eq₁ : ∀ {a A n m} xs ys (m≤n : m ℕ.≤ n) → drop′ {a} {A} m≤n ≤-refl (ys ++ xs) ≡ xs
+  eq₁ xs [] z≤n = refl
+  eq₁ xs (_ ∷ ys) (s≤s m≤n) = eq₁ xs ys m≤n
+
+  eq₂ : ∀ {a A m} ys → take′ {a} {A} {m} ≤-refl ys ≡ ys
+  eq₂ [] = refl
+  eq₂ (x ∷ ys) = cong (x ∷_) (eq₂ ys)
+
+shift≤-idem : ∀ {n i j} Γ,Δ i≤j j≤m → shift≤ {n} {i} (shift≤ {i = j} Γ,Δ j≤m) i≤j ≋ shift≤ Γ,Δ (≤-trans i≤j j≤m)
+shift≤-idem record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m = refl , eq₁ Γ Δ m≤n i≤j j≤m , eq₂ Δ i≤j j≤m
   where
-  eq : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) i j i<m .(1+j≥m : _) →
-    rotate {a} {A} i j
-      (pred-mono {_} {suc (toℕ j)} (≤-trans i<m 1+j≥m))
-      (C.cast (trans (sym (+-∸-assoc (suc m) m≤n)) (m+n∸m≡n (suc m) n)) (ys ++ xs)) ≡
-    C.cast
-      (trans (sym (+-∸-assoc m (pred-mono (≤-step m≤n)))) (m+n∸m≡n (suc m) n))
-      ( remove′ ys (λ ()) (fromℕ< i<m) ++
-        insert′ xs m≤n (λ ())
-          (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m))
-          (lookup ys (fromℕ< i<m)))
-  eq {m = zero} {suc _} xs (y ∷ []) m≤n zero zero i<m 1+j≥m = refl
-  eq {m = zero} {suc (suc _)} (x ∷ xs) (y ∷ []) _ zero (suc j) _ _ = cong (x ∷_) (eq xs (y ∷ []) (s≤s z≤n) zero j (s≤s z≤n) (s≤s z≤n))
-  eq {m = zero} {suc _} _ (_ ∷ []) _ (suc _) _ (s≤s ()) _
-  eq {m = suc _} {suc _} _ (_ ∷ _) _ _ zero _ 1+j≥m = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
-  eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n zero (suc j) i<m 1+j≥m = cong (y ∷_) (eq xs (x ∷ ys) (pred-mono m≤n) zero j (s≤s z≤n) (pred-mono 1+j≥m))
-  eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n (suc i) (suc j) (s≤s i<m) 1+j≥m = cong (x ∷_) (eq xs (y ∷ ys) (pred-mono m≤n) i j i<m (pred-mono 1+j≥m))
+  eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : i ℕ.≤ j) (j≤m : j ℕ.≤ m) →
+        drop′ {a} {A} (≤-trans j≤m m≤n) i≤j (take′ j≤m ys ++ drop′ m≤n j≤m (ys ++ xs)) ≡
+        drop′ m≤n (≤-trans i≤j j≤m) (ys ++ xs)
+  eq₁ _ _ _ z≤n z≤n = refl
+  eq₁ xs (y ∷ ys) (s≤s m≤n) z≤n (s≤s j≤m) = cong (y ∷_) (eq₁ xs ys m≤n z≤n j≤m)
+  eq₁ xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) = eq₁ xs ys m≤n i≤j j≤m
+
+  eq₂ : ∀ {a A m i j} ys (i≤j : i ℕ.≤ j) (j≤m : j ℕ.≤ m) → take′ {a} {A} i≤j (take′ j≤m ys) ≡ take′ (≤-trans i≤j j≤m) ys
+  eq₂ ys z≤n j≤m = refl
+  eq₂ (y ∷ ys) (s≤s i≤j) (s≤s j≤m) = cong (y ∷_) (eq₂ ys i≤j j≤m)
+
+-- rotate₁-shift : ∀ {n i j} Γ,Δ i≥m i≤j → rotate₁ {n} {i} {j} (shift Γ,Δ) z≤n i≤j ≋ shift (rotate₁ Γ,Δ i≥m i≤j)
+-- rotate₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≥m i≤j =
+--   refl ,
+--   eq Γ Δ m≤n i≥m i≤j ,
+--   refl
+--   where
+--   eq : ∀ {a A m n i j} xs ys (m≤n : m ℕ.≤ n) i≥m i≤j → ?
+--     -- rotate {a} {A} i j i≤j (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ xs)) ≡
+--     -- C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ rotate (reduce≥′ m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs)
+--   eq xs ys m≤n i≥m i≤j = ?
+--   -- eq {m = zero} {suc _} (x ∷ xs) [] _ zero j _ _ = sym (cast-insert xs refl j j refl x)
+--   -- eq {m = zero} (x ∷ xs) [] _ (suc i) (suc j) _ i≤j = cong (x ∷_) (eq xs [] z≤n i j z≤n (pred-mono i≤j))
+--   -- eq {m = suc _} {suc _} xs (y ∷ ys) m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = cong (y ∷_) (eq xs ys (pred-mono m≤n) i j i≥m i≤j)
+
+-- transfer-cons : ∀ {n i j} Γ,Δ i<m 1+j≥m τ → transfer {suc n} {suc i} {suc j} (cons Γ,Δ τ) (s≤s i<m) 1+j≥m ≋ cons (transfer Γ,Δ i<m (pred-mono 1+j≥m)) τ
+-- transfer-cons record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i<m 1+j≥m τ =
+--   refl , eq₁ Γ Δ m≤n (fromℕ< i<m) 1+j≥m τ , eq₂ Δ (fromℕ< i<m) τ
+--   where
+--   eq₁ : ∀ {a A m n j} xs ys (m≤n : suc m ℕ.≤ n) i 1+j≥m y → ? ≡ ?
+--     -- insert′ {a} {A} xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) 1+j≥m) (lookup (y ∷ ys) (suc i)) ≡
+--     -- insert′ xs m≤n (reduce≥′ (pred-mono (≤-step m≤n)) (pred-mono 1+j≥m)) (lookup ys i)
+--   eq₁ xs ys m≤n i 1+j≥m y = ?
+--   -- eq₁ {m = zero} {suc _} xs ys m≤n i j 1+j≥m y = refl
+--   -- eq₁ {m = suc m} xs ys m≤n i zero 1+j≥m x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+--   -- eq₁ {m = suc m} {suc _} xs (x ∷ ys) m≤n i (suc j) 1+j≥m y = refl
+
+--   eq₂ : ∀ {a A m} ys (i : Fin (suc m)) y →
+--     remove′ {a} {A} (y ∷ ys) (suc i) ≡ y ∷ remove′ ys i
+--   eq₂ (x ∷ ys) i y = refl
+
+-- transfer-shift : ∀ {n i j} (Γ,Δ : Context n) i j i<m 1+j≥m → rotate₁ (shift Γ,Δ) z≤n (pred-mono (≤-trans i<m 1+j≥m)) ≋ shift (transfer Γ,Δ i j i<m 1+j≥m)
+-- transfer-shift record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m =
+--   refl ,
+--   eq Γ Δ m≤n i j i<m 1+j≥m ,
+--   refl
+--   where
+--   eq : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) i j i<m .(1+j≥m : _) →
+--     rotate {a} {A} i j
+--       (pred-mono {_} {suc (toℕ j)} (≤-trans i<m 1+j≥m))
+--       (C.cast (trans (sym (+-∸-assoc (suc m) m≤n)) (m+n∸m≡n (suc m) n)) (ys ++ xs)) ≡
+--     C.cast
+--       (trans (sym (+-∸-assoc m (pred-mono (≤-step m≤n)))) (m+n∸m≡n (suc m) n))
+--       ( remove′ ys (λ ()) (fromℕ< i<m) ++
+--         insert′ xs m≤n (λ ())
+--           (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m))
+--           (lookup ys (fromℕ< i<m)))
+--   eq {m = zero} {suc _} xs (y ∷ []) m≤n zero zero i<m 1+j≥m = refl
+--   eq {m = zero} {suc (suc _)} (x ∷ xs) (y ∷ []) _ zero (suc j) _ _ = cong (x ∷_) (eq xs (y ∷ []) (s≤s z≤n) zero j (s≤s z≤n) (s≤s z≤n))
+--   eq {m = zero} {suc _} _ (_ ∷ []) _ (suc _) _ (s≤s ()) _
+--   eq {m = suc _} {suc _} _ (_ ∷ _) _ _ zero _ 1+j≥m = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m))
+--   eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n zero (suc j) i<m 1+j≥m = cong (y ∷_) (eq xs (x ∷ ys) (pred-mono m≤n) zero j (s≤s z≤n) (pred-mono 1+j≥m))
+--   eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n (suc i) (suc j) (s≤s i<m) 1+j≥m = cong (x ∷_) (eq xs (y ∷ ys) (pred-mono m≤n) i j i<m (pred-mono 1+j≥m))
-- 
cgit v1.2.3