--- a/eq.ur	Mon Mar 21 10:16:12 2011 -0400
+++ b/eq.ur	Tue Jun 14 08:55:15 2011 -0400
@@ -18,7 +18,7 @@
      (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
                       (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest)
                       [pre :: {K}] [pre ~ [nm = t] ++ rest] pf =>
-         f [pre] [nm] [t] [rest] ! ! pf (acc [[nm = t] ++ pre] ! pf))
+         f [pre] [nm] [t] [rest] pf (acc [[nm = t] ++ pre] pf))
      (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl
 
 fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}]
@@ -27,7 +27,7 @@
     (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r =
     @@fold [fn r' => $(mapU tr r') -> tf r'] [r]
       (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
-          f [pre] [nm] [post] ! ! pf r.nm (acc (r -- nm)))
+          f [pre] [nm] [post] pf r.nm (acc (r -- nm)))
       (fn _ => i) fl r
 
 fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
@@ -36,7 +36,7 @@
     (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r =
     @@fold [fn r' => $(map tr r') -> tf r'] [r]
       (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
-          f [pre] [nm] [t] [post] ! ! pf r.nm (acc (r -- nm)))
+          f [pre] [nm] [t] [post] pf r.nm (acc (r -- nm)))
       (fn _ => i) fl r
 
 fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
@@ -45,7 +45,7 @@
     (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r =
     @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r]
       (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 =>
-          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+          f [pre] [nm] [t] [post] pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
       (fn _ _ => i) fl r1 r2
 
 fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
@@ -54,7 +54,7 @@
     (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r =
     @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r]
       (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 =>
-          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
+          f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
       (fn _ _ _ => i) fl r1 r2 r3
 
 fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
@@ -63,7 +63,7 @@
     (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r =
     @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r]
       (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 =>
-          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
+          f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
       (fn _ _ _ _ => i) fl r1 r2 r3 r4
 
 fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}]
@@ -72,5 +72,5 @@
     (fl : folder r) (r : $(map tr r)) : $(map tf r) =
   @@foldR [tr] [fn r => $(map tf r)] [r]
       (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc =>
-          {nm = f [nm] [t] [pre ++ post] ! pf r} ++ acc)
+          {nm = f [nm] [t] [pre ++ post] pf r} ++ acc)
       {} fl r