diff options
| -rwxr-xr-x | theories/Sets/Relations_1_facts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 1b27a4a9de..c86e573182 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -28,7 +28,7 @@ Theorem Rsym_imp_notRsym: (U: Type) (R: (Relation U)) (Symmetric U R) -> (Symmetric U (Complement U R)). Proof. Unfold Symmetric Complement. -(Intros U R H' x y H'0; Red; Intro H'1; Apply H'0); Auto with sets. +Intros U R H' x y H'0; Red; Intro H'1; Apply H'0; Auto with sets. Qed. Theorem Equiv_from_preorder : |