diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 41034ce85..9d47ef72c 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -73,7 +73,7 @@ Qed. Lemma is_empty_equal_empty: is_empty s = equal s empty. Proof. apply bool_1; split; intros. -rewrite <- (empty_is_empty_1 (s:=empty)); auto with set. +auto with set. rewrite <- is_empty_iff; auto with set. Qed. |