Bug fixes: directed connection in adding vars to invariant parameters; missing `use_quants:false` in `unify` calls; pass updated `bvs` to `unify`. Sort branches: shorter premises first.