Function close_over_context_locals 

pub fn close_over_context_locals(ctx: &Context, term: &Term) -> Term

The UNIVERSAL CLOSURE of a proof term: term wrapped in a λ for every LOCAL binding of ctx that occurs free in it, so the result is closed.

A statement may mention variables free — Lean’s variable (n : Int), our ∃m. m = n + 1 — and the certifier lowers those to Term::Var, which the main kernel resolves through the context’s bindings. The independent RE-CHECKER translates to de Bruijn indices and has no notion of a context’s locals at all, so it rejects any such term as “unbound local variable” and double_check reports a disagreement about a proof both kernels would accept in closed form. Closing the term hands them the same closed object; its type is the theorem’s universal quantification, so agreement on it is strictly stronger than agreement on the open judgement.

Order is the deterministic sorted order of the names; every such binding’s type is a closed Global (Int/Entity), so the binders are independent and the order does not matter.