diff options
Diffstat (limited to 'theories/Relations/Relations.v')
| -rwxr-xr-x | theories/Relations/Relations.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 60cb9b4d7..86627c8b3 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -16,7 +16,7 @@ Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B) (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))). Intros; Split; Elim H; Red; Auto. Intros; Apply equiv_trans with (f y); Assumption. -Save. +Qed. Lemma inverse_image_of_eq : (A,B:Set)(f:A->B) (equivalence A [x,y:A](f x)=(f y)). @@ -25,4 +25,4 @@ Split; Red; | (* transitivity *) Intros; Transitivity (f y); Assumption | (* symmetry *) Intros; Symmetry; Assumption ]. -Save. +Qed. |