--- a/src/DepList.v	Mon Oct 20 09:11:54 2008 -0400
+++ b/src/DepList.v	Mon Oct 20 10:44:20 2008 -0400
@@ -52,6 +52,10 @@
       | x :: ls' => B x * hlist ls'
     end%type.
 
+  Definition hnil : hlist nil := tt.
+  Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
+    (v, hls).
+
   Variable elm : A.
 
   Fixpoint member (ls : list A) : Type :=
@@ -71,6 +75,18 @@
           | inr idx' => hget ls' (snd mls) idx'
         end
     end.
+
+  Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
+    match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
+      | nil => fun _ hls2 => hls2
+      | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
+    end.
 End hlist.
 
+Implicit Arguments hnil [A B].
+Implicit Arguments hcons [A B x ls].
 Implicit Arguments hget [A B elm ls].
+Implicit Arguments happ [A B ls1 ls2].
+
+Infix ":::" := hcons (right associativity, at level 60).
+Infix "+++" := happ (right associativity, at level 60).