blob: b97689676ba787daff22694ece50bc637b94c60f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import TestSuite.admit.
Require Setoid.
Variables P Q : forall {T : Set}, T -> Prop.
Lemma rule{T : Set}{x : T} : Q x <-> P x. admit. Qed.
Goal forall (T : Set)(x : T), Q x <-> P x.
Proof.
intros T x.
setoid_rewrite rule.
reflexivity.
Qed.
|
