The problem is like:

When I move the flattenTerms before resolveSyntaxPredicate, For some terms, the resolveSyntaxPredicate step cannot detect the isInt relation among the term's variables. For example:

  rule <k> '`,(.KList) => .K ...</k>
       <array>... P |-> (_ => V) ...</array>
       <ptr> P:Int </ptr>
       <in> ListItem(V:Int) => .List ...</in>

The resolveSyntaxPredicate step should collect the variables P and V as #andBool(isInt(P),isInt(V)). 

However, if I move the flattenTerms before resolveSyntaxPredicate, the term will become 
...
       <ptr> P:KItem </ptr>
       <in> ListItem(V:KItem) => .List ...</in>

Hence, the resolveSyntaxPredicate cannot detect the isInt relation among variables P and V.