From 423577ea49790bab2113c8d69ff8f9b6483a6015 Mon Sep 17 00:00:00 2001
From: Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@gmail.com>
Date: Sun, 17 Sep 2017 10:05:30 +0300
Subject: [PATCH] A small simplification on binnat.ctt

---
 examples/binnat.ctt | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/examples/binnat.ctt b/examples/binnat.ctt
index f156ef0..3c0ef3f 100644
--- a/examples/binnat.ctt
+++ b/examples/binnat.ctt
@@ -211,10 +211,8 @@ eqDouble2 : Path Double DoubleBinN' DoubleBinN
      rem1 : (n : binN) -> Path binN (doubleBinN' n) (doubleBinN n)
       = split
       binN0     -> <_> binN0
-      binNpos p -> <i> comp (<_> binN) (NtoBinN (doubleN (PosToN p)))
-                          [ (i=0) -> <_> NtoBinN (doubleN (PosToN p))
-                          , (i=1) -> lem1 (x0 p) ]
-
+      binNpos p -> lem1 (x0 p)
+      
 eqDouble : Path Double DoubleN DoubleBinN =
   compPath Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
 
-- 
2.34.1