diff options
Diffstat (limited to 'theories/Relations/Relations.v')
| -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 f9fb2c442..ed2567396 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -14,16 +14,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 in |- *; auto. + intros; 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 in |- *; + split; red; [ (* reflexivity *) reflexivity | (* transitivity *) intros; transitivity (f y); assumption - | (* symmetry *) intros; symmetry in |- *; assumption ]. + | (* symmetry *) intros; symmetry ; assumption ]. Qed. |