From 95c915ce89cc168ec34ab36797c78de94fcc0a18 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 17 Sep 2014 17:45:39 +0200 Subject: Add some missing Proof statements. --- theories/Setoids/Setoid.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories/Setoids') 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. -- cgit v1.2.3