subtype: generalize over section-declared free types at section close

[strub]

[subtype X = { x : T | P x }] declared inside [section. declare type
c. ...] previously stayed monomorphic at section close. The cloned
auto-axioms ([insubN], [insubT], [valP], [valK]) and the [val] / [insub]
operators correctly gained a [c] tparam, but [X] itself didn't — the
result was an inconsistent state where the operations were polymorphic
over [c] but returned a single shared [X] type for every instantiation,
a soundness gap flagged by [FIXME:SUBTYPE] at [add_subtype].

This patch threads the carrier and predicate through the subtype's
[tydecl] so [tydecl_fv] picks up their dependency on section-declared
free types and the existing [generalize_tydecl] machinery adds the
right tparams at close.

Tests in [tests/subtype-section-generalize.ec] cover three cases:

1. carrier mentions a section-declared free type — subtype is unary.
2. predicate mentions a section-declared free type (carrier doesn't) —
   same outcome via fv collected from the predicate.
3. nested sections, subtype declared in the inner one, depending on
   free types from both levels — subtype is binary after both closes.
   Each test instantiates [val] and [valP] at two distinct carriers in a
   single lemma; would fail to type-check if the cloned type or axiom
   had stayed monomorphic.

Closes #1001

[oskgo]

Looks like this handles all the edge cases I had found. Awesome!

I think there were some theories where I was using an inlined Subtype or Quotient construction because of this. I need to get around to migrating those now.

[fdupress]

Be careful that the "update" button creates a merge commit by default. You need to open the drop-down and select "Update by rebase"

[strub]

Yes. I only have my phone. So not hesitate to revert the merge and rebase. (The CI will forbid merging it anyway)