--- a/src/MoreDep.v	Tue Oct 07 21:58:45 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 22:05:37 2008 -0400
@@ -478,7 +478,7 @@
       | Black => { c' : color & rbtree c' n }
     end.
 
-  Definition makeBlack c n : insResult c n -> insertResult c n :=
+  Definition makeRbtree c n : insResult c n -> insertResult c n :=
     match c return insResult c n -> insertResult c n with
       | Red => fun r =>
         match r in rtree n return insertResult Red n with
@@ -487,16 +487,10 @@
       | Black => fun r => r
     end.
 
-  Implicit Arguments makeBlack [c n].
+  Implicit Arguments makeRbtree [c n].
 
   Definition insert c n (t : rbtree c n) : insertResult c n :=
-    makeBlack (ins t).
-
-  Record rbtree' : Set := Rbtree' {
-    rtC : color;
-    rtN : nat;
-    rtT : rbtree rtC rtN
-  }.
+    makeRbtree (ins t).
 
   Section present.
     Variable z : nat.
@@ -577,20 +571,21 @@
           tauto.
     Qed.
 
+    Ltac present_insert t :=
+      unfold insert; inversion t;
+        generalize (present_ins t); simpl;
+          dep_destruct (ins t); tauto.
+
     Theorem present_insert_Red : forall n (t : rbtree Red n),
       present z (insert t)
       <-> (z = x \/ present z t).
-      unfold insert; inversion t;
-        generalize (present_ins t); simpl;
-          dep_destruct (ins t); tauto.
+      intros; present_insert t.
     Qed.
 
     Theorem present_insert_Black : forall n (t : rbtree Black n),
       present z (projT2 (insert t))
       <-> (z = x \/ present z t).
-      unfold insert; inversion t;
-        generalize (present_ins t); simpl;
-          dep_destruct (ins t); tauto.
+      intros; present_insert t.
     Qed.
   End present.
 End insert.