From 185e7991bbc4c78a5e729a3584a51ae453b9eb79 Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Sat, 21 Sep 2024 12:09:48 +0100
Subject: [PATCH] Removed dinaturality sorries

---
 .../BinSyntax/Rewrite/Region/Uniform.lean     | 31 +++++++++++++++++--
 1 file changed, 28 insertions(+), 3 deletions(-)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean
index 2f343e7..1de0c73 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean
@@ -505,9 +505,34 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
             add_tsub_cancel_right, vsubst0_var0_vwk1]
           rfl
           simp [vsubst0_var0_vwk1]
-      · funext i
-        sorry
-    · sorry
+      · funext i; congr
+        funext k
+        simp [Subst.vlift, Subst.extend, Subst.liftn, Subst.comp]
+        split
+        · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
+          Subst.extend, ↓reduceIte, vsubst0_var0_vwk1, *]
+          simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1]
+        · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
+          Subst.liftn, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right,
+          vsubst0_var0_vwk1]
+          simp only [vwk1_lwk]
+          simp only [← lsubst_fromLwk, lsubst_lsubst]
+          congr
+          funext j
+          simp [Subst.comp, Subst.vlift, Subst.extend]
+    · simp [lsubst_lsubst]
+      funext i; congr; funext k;
+      simp [Subst.vlift, Subst.liftn, Subst.comp, Subst.fromFCFG]
+      split
+      · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
+        Subst.fromFCFG, ↓reduceDIte, vsubst0_var0_vwk1, *]
+        simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1]
+      · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.liftn,
+        add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1]
+        simp only [vwk1_lwk]
+        simp only [← lsubst_fromLwk, lsubst_lsubst]
+        congr
+        funext j; simp [Subst.comp, Subst.fromFCFG, Subst.vlift]
 
 theorem Uniform.vsubst_flatten {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ Δ L r r'}
   (toVsubst : ∀{Γ Δ L σ r r'}, σ.Wf Γ Δ → P Δ L r r' → Uniform P Γ L (r.vsubst σ) (r'.vsubst σ))