Add ext_eq axiom and DepList notations

Makefile

-MODULES_NODOC := Tactics MoreSpecif DepList
+MODULES_NODOC := Axioms Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality

src/Axioms.v

+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* Additional axioms not in the Coq standard library *)
+
+Axiom ext_eq : forall (A : Type) (B : A -> Type)
+  (f g : forall x, B x),
+  (forall x, f x = g x)
+  -> f = g.
+
+Ltac ext_eq := apply ext_eq; intro.

src/DepList.v

@@ -52,6 +52,10 @@ Section hlist.
       | 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 @@ Section hlist.
           | 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).