1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index f49f58e5..be5999df 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
+
+(* Submitted by Nicolas Tabareau *)
+(* Needs unification.ml to support environments with de Bruijn *)
+
+Goal forall
+  (f : Prop -> Prop)
+  (Q : (nat -> Prop) -> Prop)
+  (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
+  (h:nat -> Prop), 
+  Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
+intros f0 Q H.
+setoid_rewrite H.
+tauto.
+Qed.