Small improvements

Fix t_unify_ind to remember that the substitution is well-founded.

Add a theorem that the free unification variables of a (walkstar s t) are not
in the domain of s.