diff options
Diffstat (limited to 'theories/Setoids/Setoid.v')
| -rw-r--r-- | theories/Setoids/Setoid.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index eec7aa2d7..2ffe70bff 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -16,14 +16,17 @@ Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. +Proof. unfold Setoid_Theory in s. intros ; reflexivity. Defined. Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. +Proof. unfold Setoid_Theory in s. intros ; symmetry ; assumption. Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. +Proof. unfold Setoid_Theory in s. intros ; transitivity y ; assumption. Defined. |