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