diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /test-suite/success/setoid_test.v | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'test-suite/success/setoid_test.v')
| -rw-r--r-- | test-suite/success/setoid_test.v | 14 |
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. |