--- a/src/DepList.v	Mon Oct 20 10:44:20 2008 -0400
+++ b/src/DepList.v	Mon Oct 20 12:17:39 2008 -0400
@@ -64,6 +64,11 @@
       | x :: ls' => (x = elm) + member ls'
     end%type.
 
+  Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
+    inl _ pf.
+  Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
+    inr _ m.
+
   Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
     match ls return hlist ls -> member ls -> B elm with
       | nil => fun _ idx => match idx with end
@@ -88,5 +93,8 @@
 Implicit Arguments hget [A B elm ls].
 Implicit Arguments happ [A B ls1 ls2].
 
+Implicit Arguments hfirst [A elm x ls].
+Implicit Arguments hnext [A elm x ls].
+
 Infix ":::" := hcons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).