test-suite/complexity/setoid_rewrite.v


1
2
3
4
5
6
7
8
9
10

(* Check bug #1176 *)
(* Expected time < 0.50s *)

Require Import Setoid.

Variable f : nat -> Prop.

Goal forall U:Prop, f 100 <-> U.
intros U.
Time setoid_replace U with False.