Prove renaming is fully congruent.less-fin

1 files changed, 30 insertions, 0 deletions

diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda
index 8e862ed..e9d26ea 100644
--- a/src/Data/Type/Properties.agda
+++ b/src/Data/Type/Properties.agda
@@ -499,3 +499,33 @@ rename-congˡ A [ρs₁]≗[ρs₂] =
   Wf.All.wfRec (On.wellFounded size <-wellFounded) _
     Rename.IH Rename.rename-helper
     A (Rename.do-congˡ [ρs₁]≗[ρs₂])
+
+rename-congʳ : ∀ ρs → A ≈ B → rename ρs A ≈ rename ρs B
+rename-congʳ ρs (var α)                   = var _
+rename-congʳ ρs unit                      = unit
+rename-congʳ ρs (bin A≈C B≈D)             =
+  bin (rename-congʳ ρs A≈C) (rename-congʳ ρs B≈D)
+rename-congʳ ρs (all {α} {A} {β} {B} A≈B) = all (λ {γ} ∉₁ ∉₂ → begin
+  rename ((α′ , γ) ∷ []) (rename ((α , α′) ∷ ρs) A)
+    ≈⟨  rename-∘ ((α , α′) ∷ ρs) _ A ⟩
+  rename ((α , α′) ∷ ρs ++ (α′ , γ) ∷ []) A
+    ≈˘⟨ rename-∘ ((α , α′) ∷ []) _ A ⟩
+  rename (ρs ++ (α′ , γ) ∷ []) (rename ((α , α′) ∷ []) A)
+    ≈⟨  rename-congʳ ((ρs ++ (α′ , γ) ∷ [])) (A≈B α′∉∀α∙A α′∉∀β∙B) ⟩
+  rename (ρs ++ (α′ , γ) ∷ []) (rename ((β , α′) ∷ []) B)
+    ≈⟨  rename-∘ (((β , α′) ∷ [])) _ B ⟩
+  rename ((β , α′) ∷ ρs ++ (α′ , γ) ∷ []) B
+    ≡⟨  cong
+          ((λ δ → rename ((β , δ) ∷ ρs ++ (δ , γ) ∷ []) B) ∘ mkFresh ∘ (_++ _))
+          (free-≈ (all A≈B)) ⟩
+  rename ((β , β′) ∷ ρs ++ (β′ , γ) ∷ []) B
+    ≈˘⟨ rename-∘ ((β , β′) ∷ ρs) _ B ⟩
+  rename ((β′ , γ) ∷ []) (rename ((β , β′) ∷ ρs) B)
+    ∎)
+  where
+  αs = free (all α A) ++ map Subst.from ρs ++ map Subst.to ρs
+  α′ = mkFresh αs
+  β′ = mkFresh (free (all β B) ++ map Subst.from ρs ++ map Subst.to ρs)
+  α′∉∀α∙A = isFresh .distinct αs ∘ ∈-++⁺ˡ
+  α′∉∀β∙B = P.subst (α′ ∉_) (free-≈ (all A≈B)) α′∉∀α∙A
+  open ≈-Reasoning