1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
Require Import FSets.
Module SomeSetoids (Import M:FSetInterface.S).
Lemma Equal_refl : forall s, s[=]s.
Proof. red; split; auto. Qed.
Add Relation t Equal
reflexivity proved by Equal_refl
symmetry proved by eq_sym
transitivity proved by eq_trans
as EqualSetoid.
Add Morphism Empty with signature Equal ==> iff as Empty_m.
Proof.
unfold Equal, Empty; firstorder.
Qed.
End SomeSetoids.
Module Test (Import M:FSetInterface.S).
Module A:=SomeSetoids M.
Module B:=SomeSetoids M. (* lots of warning *)
Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
intros.
rewrite H in H0.
assumption.
Qed.
End Test.
|
