The current unification algorithm doesn't handle
ExprPred very well. For example, the predicate A \land
B can be parsed as
<ExprPred>
<AndExpr>...</AndExpr>
<ExprPred>
or as
<AndPred>
<ExprPred>...</ExprPred>
<ExprPred>...</ExprPred>
</AndPred>
These are semantically equivalent but don't unifiy at
the moment. It would be nice to improve the
unification so that they do unify.