--- a/variant.urs	Mon Jan 02 17:23:31 2012 -0500
+++ b/variant.urs	Thu Jan 05 18:04:04 2012 -0500
@@ -10,6 +10,9 @@
                                                                     -> variant ([nm = t] ++ ts) -> option t
 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
 
+val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1
+             -> variant r1 -> variant (r1 ++ r2)
+
 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
     Eq.eq r ([nm = t] ++ ts)
     -> folder r
@@ -22,6 +25,8 @@
     -> f t
     -> variant (map f r)
 
+val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r)
+
 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
 
 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
@@ -29,6 +34,8 @@
 val appR : m ::: (Type -> Type) -> monad m
            -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
 
+val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)
+
 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
              -> (p :: K -> f p -> fr p -> t)
              -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t