blob: e594e96936b2cbb0ebedca915fc2a97adf8f99c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
Section Bug.
Context {A : Type} (R : relation A).
Hypothesis pre : PreOrder R.
Context `{SA : Setoid A}.
Goal True.
set (SA' := SA).
assert ( forall SA0 : Setoid A,
@PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
rename SA into SA0.
intro SA.
admit.
admit.
Qed.
End Bug.
|
