FOL existentials

[koo5]

We need a better story on FOL existential variables. They could appear in either the body or the head of a rule. We don't support the body case. What should really happen in the head case?
Presumably, it asserts that there exists some object of given properties.
Is there a theory that allows us to specify under what conditions is this object equal to another?
http://www.lirmm.fr/~mugnier/graphik/kiabora/

...
Is there a story on supporting or not supporting complex terms? functions?

what are the objectives (mltt typechecking..)?