diff options
Diffstat (limited to 'theories/FSets/FSetEqProperties.v')
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ac08351ad9..7618880bd2 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -460,9 +460,11 @@ Qed. End BasicProperties. +#[global] Hint Immediate empty_mem is_empty_equal_empty add_mem_1 remove_mem_1 singleton_equal_add union_mem inter_mem diff_mem equal_sym add_remove remove_add : set. +#[global] Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1 choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal subset_refl subset_equal subset_antisym |