hunk ./Data/Witness/List.hs 65
-    listFill :: (forall a. w a -> a) -> ListType w t -> t;
-    listFill _f NilListType = ();
-    listFill f (ConsListType w rest) = (f w,listFill f rest);
+    listFill :: ListType w t -> (forall a. w a -> a) -> t;
+    listFill NilListType _f = ();
+    listFill (ConsListType wa wr) f = (f wa,listFill wr f);
+
+    listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t;
+    listMap NilListType _f () = ();
+    listMap (ConsListType wa wr) f (a,rest) = (f wa a,listMap wr f rest);
+
+    listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t;
+    listLift2 NilListType _f () () = ();
+    listLift2 (ConsListType wa wr) f (a,resta) (b,restb) = (f wa a b,listLift2 wr f resta restb);
hunk ./Data/Witness/List.hs 232
-        listMap :: cc l lr
+        listMapW :: cc l lr
hunk ./Data/Witness/List.hs 239
-        listMap = tensorUnit
+        listMapW = tensorUnit
hunk ./Data/Witness/List.hs 243
-        MkMapList wit listMap' -> mapwit w (\w' vmap -> MkMapList
+        MkMapList wit listMapW' -> mapwit w (\w' vmap -> MkMapList
hunk ./Data/Witness/List.hs 246
-            listMap = tensorPair vmap listMap'
+            listMapW = tensorPair vmap listMapW'