From d65d60fe31f0c25c7e845d66e37c47e4f22924e1 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 22 Feb 2024 11:22:01 -0600
Subject: Fill in omitted proof

---
 FinMerge.agda            |  8 ++++----
 FinMerge/Properties.agda | 18 +++++++++++++++++-
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/FinMerge.agda b/FinMerge.agda
index 2e0ad03..51e7a67 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -50,10 +50,10 @@ glue-iter
     → Σ[ x ∈ ℕ ] (Fin n → Fin x)
 glue-iter {ℕ.zero} {n} {y} f g h = y , h
 glue-iter {ℕ.suc m} {n} {y} f g h with compare (f (# 0)) (g (# 0))
-... | less (f0<g0 , s≤s g0<n) =
-        let p = merge (f0<g0 , g0<n) in
+... | less (f0<g0 , s≤s g0≤n) =
+        let p = merge (f0<g0 , g0≤n) in
         glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
 ... | equal _ = glue-iter (f ∘ Fin.suc) (g ∘ Fin.suc) h
-... | greater (g0<f0 , s≤s f0<n) =
-        let p = merge (g0<f0 , f0<n) in
+... | greater (g0<f0 , s≤s f0≤n) =
+        let p = merge (g0<f0 , f0≤n) in
         glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda
index 6d6c964..e403d99 100644
--- a/FinMerge/Properties.agda
+++ b/FinMerge/Properties.agda
@@ -111,7 +111,23 @@ glue-iter-append
     → (f g : Fin m → Fin y)
     → (h : Fin n → Fin y)
     → Σ[ h′ ∈ (Fin y → Fin (proj₁ (glue-iter f g h))) ] (proj₂ (glue-iter f g h) ≡ h′ ∘ h)
-glue-iter-append f g h = ?
+glue-iter-append {ℕ.zero} f g h = id , refl
+glue-iter-append {ℕ.suc m} f g h with compare (f (# 0)) (g (# 0))
+glue-iter-append {ℕ.suc m} f g h | less (f0<g0 , s≤s g0≤n)
+  with
+    glue-iter-append
+        (merge (f0<g0 , g0≤n) ∘ f ∘ Fin.suc)
+        (merge (f0<g0 , g0≤n) ∘ g ∘ Fin.suc)
+        (merge (f0<g0 , g0≤n) ∘ h)
+... | h′ , glue-p∘h≡h′∘p∘h = h′ ∘ merge (f0<g0 , g0≤n) , glue-p∘h≡h′∘p∘h
+glue-iter-append {ℕ.suc m} f g h | equal x = glue-iter-append (f ∘ Fin.suc) (g ∘ Fin.suc) h
+glue-iter-append {ℕ.suc m} f g h | greater (g0<f0 , s≤s f0≤n)
+  with
+    glue-iter-append
+        (merge (g0<f0 , f0≤n) ∘ f ∘ Fin.suc)
+        (merge (g0<f0 , f0≤n) ∘ g ∘ Fin.suc)
+        (merge (g0<f0 , f0≤n) ∘ h)
+... | h′ , glue-p∘h≡h′∘p∘h = h′ ∘ merge (g0<f0 , f0≤n) , glue-p∘h≡h′∘p∘h
 
 lemma₂
     : (f g : Fin (ℕ.suc m) → Fin n)
-- 
cgit v1.2.3