From e7272333cb45c090702efebe4436568306caa1a8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 1 Nov 2022 21:05:04 +0100
Subject: [PATCH] remove a believe_me

---
 lib/Quox/Syntax/Shift.idr | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index 9face99..d033d61 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -110,7 +110,14 @@ export
 ssDownEqv SZ      = EqSS EqSZ
 ssDownEqv (SS by) = EqSS $ ssDownEqv by
 
-%transform "Shift.ssDown" ssDown by = believe_me (SS by)
+private
+ssDownViaNat : Shift (S from) to -> Shift from to
+ssDownViaNat by =
+  rewrite shiftDiff by in
+  rewrite sym $ plusSuccRightSucc by.nat from in
+  fromNat $ S by.nat
+
+%transform "Shift.ssDown" ssDown = ssDownViaNat
 
 
 public export