1
Require Export Relation_Definitions.
5
Variable S : A -> Type.
6
Variable Seq : forall {a:A}, relation (S a).
8
Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
9
Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
10
Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
13
Add Parametric Relation a : (S a) Seq
14
reflexivity proved by Seq_refl
15
symmetry proved by Seq_sym
16
transitivity proved by Seq_trans
19
Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
21
setoid_replace x with y.