From a2bca9eb599e8109ba91e257ee223b39f64703c1 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 5 Mar 2021 16:16:42 +0000
Subject: Remove incomplete unrolling proof.

---
 src/Cfe/Expression/Properties.agda | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 9af0d70..e810ce4 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -189,17 +189,6 @@ subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
   insert′ x≈y xs≋ys F.zero = x≈y ∷ xs≋ys
   insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
 
-unroll : ∀ {n} → (e : Expression (suc n)) → μ e ≋ e [ μ e / F.zero ]
-unroll e γ = begin
-  ⟦ μ e ⟧ γ ≈⟨ {!!} ⟩
-  (λ X → ⟦ e ⟧ (X ∷ γ)) (⟦ μ e ⟧ γ) ≡⟨⟩
-  ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ≡⟨⟩
-  ⟦ e ⟧ (insert γ F.zero (⟦ μ e ⟧ γ)) ≈˘⟨ subst-fun e (μ e) F.zero γ ⟩
-  ⟦ e [ μ e / F.zero ] ⟧ γ ∎
-  where
-  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
-  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
-
 monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
 monotone ⊥ γ≤γ′ = ≤-refl
 monotone ε γ≤γ′ = ≤-refl
-- 
cgit v1.2.3