+(* Uniques *)
+Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
+Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".
+Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
+Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
+ Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
+Variable unique_eq : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
+ Extract Inlined Constant unique_eq => "(==)".
+Variable unique_toString : Unique -> string.
+ Extract Inlined Constant unique_toString => "show".
+Instance EqDecidableUnique : EqDecidable Unique :=
+ { eqd_dec := unique_eq }.
+Instance EqDecidableToString : ToString Unique :=
+ { toString := unique_toString }.
+
+Inductive UniqM {T:Type} : Type :=
+ | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
+ Implicit Arguments UniqM [ ].
+
+Instance UniqMonad : Monad UniqM :=
+{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
+; bindM := fun a b (x:UniqM a) (f:a->UniqM b) =>
+ uniqM (fun u =>
+ match x with
+ | uniqM fa =>
+ match fa u with
+ | Error s => Error s
+ | OK (u',va) => match f va with
+ | uniqM fb => fb u'
+ end
+ end
+ end)
+}.
+
+Definition getU : UniqM Unique :=
+ uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
+
+Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
+Notation "'return' x" := (returnM x) (at level 100).
+Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100).
+
+
+
+
+
+
+Record FreshMonad {T:Type} :=
+{ FMT : Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh : forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT : FreshMonad >-> Funclass.
+
+
+
+Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
+
+
+
+
+Ltac eqd_dec_refl X :=
+ destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
+ [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
+
+Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
+ intros T.
+ induction t1; intros.
+ destruct t2.
+ auto.
+ inversion H.
+ destruct t2.
+ inversion H.
+ simpl in H.
+ inversion H.
+ set (IHt1 _ H2) as q.
+ rewrite q.
+ reflexivity.
+ Qed.
+
+(* adapted from Adam Chlipala's posting to the coq-club list (thanks!) *)
+Definition openVec A n (v: vec A (S n)) : exists a, exists v0, v = a:::v0 :=
+ match v in vec _ N return match N return vec A N -> Prop with
+ | O => fun _ => True
+ | S n => fun v => exists a, exists v0, v = a:::v0
+ end v with
+ | vec_nil => I
+ | a:::v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
+ end.
+
+Definition nilVec A (v: vec A O) : v = vec_nil :=
+ match v in vec _ N return match N return vec A N -> Prop with
+ | O => fun v => v = vec_nil
+ | S n => fun v => True
+ end v with
+ | vec_nil => refl_equal _
+ | a:::v0 => I
+ end.
+
+Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+ intros.
+ induction n.
+ set (nilVec _ v1) as v1'.
+ set (nilVec _ v2) as v2'.
+ subst.
+ simpl.
+ reflexivity.
+ set (openVec _ _ v1) as v1'.
+ set (openVec _ _ v2) as v2'.
+ destruct v1'.
+ destruct v2'.
+ destruct H.
+ destruct H0.
+ subst.
+ simpl.
+ rewrite IHn.
+ reflexivity.
+ Qed.