1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
Require Import Setoid.
Set Printing Existential Instances.
Axiom A : Type.
Axiom i : A.
Axiom Equal : A -> A -> Prop.
Axiom P : A -> Prop.
Axiom everything_equal : forall (j : A), Equal i j.
Instance b : Morphisms.Proper (Equal ==> Basics.impl) P. Admitted.
Axiom forget : P i -> A.
Lemma blah (H : P i) : True.
unshelve rewrite everything_equal in H.
Fail exact (forget H).
Abort.
Lemma blah (H : P i) : True.
unshelve setoid_rewrite everything_equal in H.
Fail exact (forget H).
Abort.
|
