The treatment of existential variables is a bit hacked now. Bill McCune? has pointed to Champeaux's procedure (the paper attached here), however it requires (anti)skolemization for each pair of tested formulas, so I'll have to think how to do efficient indexing (possibly cheaply in E) for this. The procedure however seems directly usable instead of the Mizar Unifier (see AndrzejTrybulec?'s description of that at http://www.cs.ru.nl/~freek/mizar/by.ps.gz).