 
       ;; Unifying an lvar with some other value creates a new entry in
       ;; the substitution map
-      u-is-lvar (assoc s-map u v)
-      v-is-lvar (assoc s-map v u)
+      u-is-lvar (add-substitution s-map u v)
+      v-is-lvar (add-substitution s-map v u)
 
       ;; Unifying two non-lvars is delegated to the polymorphic
       ;; `unify-terms` function, from IUnifyTerms.

  nil
  (walk [u s-map] nil))

;; ## <a name="unification"></a>Unification

(defn unify

(extend-protocol IReifySubstitution
  LVar
  (reify-s* [v s-map] (let [n (reify-name (count s-map))]
                        (add-substitution s-map v n)))

  Object
  (reify-s* [v s-map] s-map)

  nil
  (reify-s* [v s-map] s-map))


