blob: 0150c25038f05c0d28a926d59ebc150acc0fc0ea (
plain)
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 Export Relation_Definitions.
Require Export Setoid.
Variable A : Type.
Variable S : A -> Type.
Variable Seq : forall {a:A}, relation (S a).
Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
Seq x z.
Add Parametric Relation a : (S a) Seq
reflexivity proved by Seq_refl
symmetry proved by Seq_sym
transitivity proved by Seq_trans
as S_Setoid.
Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
intros a x y H.
setoid_replace x with y.
reflexivity.
trivial.
Qed.
|
