Function elaborate_anon_ctor 

pub fn elaborate_anon_ctor(
    ctx: &Context,
    mctx: &mut MetaCtx,
    expected: &Term,
    fields: &[Term],
) -> KernelResult<Term>

Elaborate an ANONYMOUS CONSTRUCTOR ⟨f₀, …, fₙ⟩ (E3) against an EXPECTED inductive/ structure type H a…. It applies H’s (unique) constructor to the type parameters a…, read off the expected type, then the field values — so ⟨Zero, true⟩ expected at Prod Nat Bool becomes Prod_mk Nat Bool Zero true. Each field is elaborated against its declared type (so coercions/implicits fire), and the whole is kernel-certified.