diff options
| -rw-r--r-- | theories/Relations/Relations.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 0a5128f093..dea76694f3 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -16,16 +16,16 @@ Lemma inverse_image_of_equivalence : forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). Proof. - intros; split; elim H; red; auto. + intros A B f r H; split; elim H; red; auto. intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. Lemma inverse_image_of_eq : forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. - split; red; + intros A B f; split; red; [ (* reflexivity *) reflexivity - | (* transitivity *) intros; transitivity (f y); assumption + | (* transitivity *) intros x y z; transitivity (f y); assumption | (* symmetry *) intros; symmetry ; assumption ]. Qed. |