fix(hax-lib): Fix refinement macro in presence of generics.

[maximebuyse]

Fixes #899 . Claude generated.

Root cause

#[hax_lib::attributes] on a struct generates, for each
#[refine(...)]-annotated field, a hidden refinement function whose
parameters are the struct's fields:

fn refinement(indices: [u8; LEN]) -> ::hax_lib::Prop { ... }

This function was generated without the struct's generics. So when a field
type (or the refinement formula) mentions a const generic such as LEN, that
parameter is out of scope.

Under hax extraction (which actually compiles this #[cfg(hax_compilation)]
item) this produced:

error[E0425]: cannot find value `LEN` in this scope

and, in the engine, the field list and the refinement function's parameter
list then went out of sync, surfacing as the reported error:

[HAX0001] (FStar backend) something is not implemented yet.
associated_refinement_in_type: zip two lists of different lengths

The fix

In hax-lib/macros/src/implementation.rs, the struct's generics are now
propagated to the generated refinement function. Generic defaults are
stripped (they are not allowed on function generics) and the where-clause is
carried along:

fn refinement #generics (#binders) -> ::hax_lib::Prop #where_clause {
::hax_lib::Prop::from(#refine) }

Unused generics are harmless on functions, so this is safe for any struct
shape (type params, const params, lifetimes, and combinations).

After the fix, the reproducer extracts to a correct refined F* type:

type t_Foo (v_LEN: usize) = {
  f_indices:f_indices:
  t_Array u8 v_LEN
    { forall (i: usize).
        b2t (i <. (Core_models.Slice.impl__len #u8 (f_indices <: t_Slice u8) 
<: usize) <: bool) ==>
        b2t ((cast (f_indices.[ i ] <: u8) <: usize) <. mk_usize 2 <: bool) }
}