diff --git a/sample5.v b/sample5.v
index 6f10f9bba2e148320b0af2975ad881020eb8f0b2..b41f9e0af76e1f0f62920777e31a6e1d8de3d5a8 100644
--- a/sample5.v
+++ b/sample5.v
@@ -99,10 +99,3 @@ apply (redo_rev_tree_elim (fun t x => x = rev_tree t)).
 intros a t1 t2 IH1 IH2; simpl; rewrite IH1, IH2.
 easy.
 Qed.
-
-Equations redo_rev_tree' {T} (t : btree T) : btree T :=
-  redo_rev_tree' t by rec t (@ltt T) :=
-  redo_rev_tree' Leaf := Leaf ;
-  redo_rev_tree' (Node a t1 t2) := Node a (redo_rev_tree t2)
-                                        (redo_rev_tree t1).
- .