Fix inconsistent arguments of `subset_difference_elem_of`.

Hu, that is strange, how did this happen?

Anyway, LGTM. Should this get a changelog entry? It's technically breaking.

It was introduced in !13 (diffs) as some helper lemma for defining a well-founded recursive function.

I don't a changelog entry is needed. I think we have changed implicit arguments in the past without.

If you prefer to have a changelog entry, I could add it.

Grepping found zero users of this lemma, so... seems fine.^^

Thanks and merged!

mentioned in commit cc9683cb

merged