Function instantiate_codomain 

pub fn instantiate_codomain(
    param: &str,
    domain: &Term,
    body: &Term,
    argument: &Term,
) -> Term

Substitute replacement for var in body, WRITING IT ONCE when copying it would blow the result up.

Term is a named tree with no sharing, so the ordinary substitution materialises a full clone of the argument at every occurrence. In a DEPENDENT telescope — a variable-heavy section, a bundled algebraic structure, Mathlib’s daily shape — the bound variable occurs once or twice per binder, so one argument becomes 2n copies and the inferred type is superlinear in the telescope depth. Lean pays nothing for this: its Expr is a hash-consed DAG over de Bruijn indices.

LOGOS’s equivalent is ζ: let x : A := a in B is definitionally B[x := a], and it writes a ONCE. The decision is a COST MODEL rather than a threshold — share exactly when the duplication would more than double the result — so the common case (a small argument, or one occurrence) is byte-identical to eager substitution and nothing downstream sees a change. Instantiate a Pi codomain while retaining the kernel’s sharing strategy. This constructs a type expression only; callers must separately establish that the function has this Pi type and the argument has its domain.