This modules implements extended substitution of DB variables in a term. This is typically used to: 1) infer a "most general" typing substitution from constraints gathered while inferring the type of the LHS of a rule. 2) apply the substitution to the RHS of the rule before typechecking it.