As a rule of thumb, if a theorem of the form is in the database, and the "more precise" theorems and also hold (see bj-bisym), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex (and equsalh and equsexh). Even if only one of these two theorems holds, it should be added to the database.