Module unify 

Structs

Substitution

Vec-based substitution with trail for efficient backtracking. Bindings are stored in a Vec indexed by VarId (O(1) lookup/bind). The trail records which VarIds were bound, enabling undo on backtracking.