From 050206a1ba06d588879171698f2f8120a8b550d4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 30 Mar 2021 18:52:46 +0100
Subject: Attempt to prove unrolling.

---
 src/Cfe/Expression/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Cfe/Expression/Base.agda')

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 1cd57a7..aabab1b 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -100,5 +100,5 @@ rank (μ e) = suc (rank e)
 
 infix 4 _<ᵣₐₙₖ_
 
-_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _
-_<ᵣₐₙₖ_ = ℕ._<_ on rank
+_<ᵣₐₙₖ_ : ∀ {m n} → REL (Expression m) (Expression n) _
+e <ᵣₐₙₖ e′ = rank e ℕ.< rank e′
-- 
cgit v1.2.3