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

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

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

(defn unify


      ;; Unifying an lvar with some other value creates a new entry in
      ;; the substitution map
      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.
