chore(logic/small): reduce imports (#7777)
By delaying the `fintype` and `encodable` instances for `small`, I think we can now avoid importing `algebra` at all into `logic`.
~~Since some of the `is_empty` lemmas haven't been used yet,~~ I took the liberty of making some arguments explicit, as one was painful to use as is.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
