diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:45:39 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-09-17 17:54:39 +0200 |
| commit | 95c915ce89cc168ec34ab36797c78de94fcc0a18 (patch) | |
| tree | a07639d54aeebdf0dd8f75f3ec0e4ccfc8e03163 /theories/Setoids | |
| parent | 9060a941d8b7566220f6fb6a191ac2fd7eca7315 (diff) | |
Add some missing Proof statements.
Diffstat (limited to 'theories/Setoids')
| -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. |