From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- test-suite/success/setoid_test.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'test-suite/success/setoid_test.v') 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. -- cgit v1.2.3