code: private PExp getImpliesExists(AMapCompMapExp exp, ILexNameToken finmap,
  			ILexNameToken findex)
  	{
  		AExistsExp exists = new AExistsExp();
  		exists.setBindList(getSetBindList(finmap, findex));
  		exists.setPredicate(getExistsPredicate(exp, finmap, findex));
  		return exists;
  	}
docs: exists idx in set dom m & m(idx) = { a |-> b }