More usable form of KK (and relatives)

It would be nice to have
```lean
theorem kruskal_katona' {r : ℕ} {𝒜 𝒞 : finset (finset ℕ)}
(h₁ : all_sized 𝒜 r) (h₂ : 𝒜.card = 𝒞.card) (h₃ : is_init_seg_of_colex 𝒞 r) :
(∂𝒞).card ≤ (∂𝒜).card :=
begin
```
Note how the types of `𝒜` and `𝒞` are changed to `finset (finset ℕ)`, instead of `finset (finset (fin n))`.

Mathematically, this isn't any harder, but there's a couple of details to take care of to formalise. Some of the commented out code around line 200 in `kruskal_katona.lean` might help with this.

Open kruskal_katona.lean and inspect the commented-out code around line 200; it may show how the existing finite-universe theorem can be adapted. Work toward the requested kruskal_katona' statement using finset (finset ℕ), and verify that the theorem and its supporting details typecheck.

Written by the indexing model from the issue text.