Function unify_in 

pub fn unify_in(
    ctx: &Context,
    mctx: &mut MetaCtx,
    lctx: &[(String, Term)],
    a: &Term,
    b: &Term,
) -> bool

Unify a and b under a LOCAL CONTEXT lctx ((name, type) of the bound variables in scope). The local context enables higher-order PATTERN (Miller) unification: ?M x̄ =?= t, where ?M is a metavariable applied to distinct bound variables x̄, is solved by ?M := λx̄. t. The top-level unify runs with an empty context, so its behavior — and every existing caller — is the first-order one.