verification fixes for MInt

@andreistefanescu please review
The integer equivalent of this lemma is causing mulitplication by addition to prove where otherwise it fails with the following output:

```
java.lang.UnsupportedOperationException: missing SMTLib translation for isKResult
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:350)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:556)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:385)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:556)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:307)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.accept(SymbolicConstraint.java:1506)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.translateConstraint(KILtoSMTLib.java:123)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.checkUnsat(SymbolicConstraint.java:837)
	at org.kframework.backend.java.kil.ConstrainedTerm.unifyImpl(ConstrainedTerm.java:263)
	at org.kframework.backend.java.kil.ConstrainedTerm.unify(ConstrainedTerm.java:213)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.getUnificationResults(SymbolicRewriter.java:384)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:243)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:293)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:666)
	at org.kframework.backend.java.symbolic.JavaSymbolicKRun.prove(JavaSymbolicKRun.java:209)
	at org.kframework.krun.KRunFrontEnd.normalExecution(KRunFrontEnd.java:132)
	at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:491)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:40)
	at org.kframework.main.Main.main(Main.java:86)
java.lang.UnsupportedOperationException: missing SMTLib translation for 'functionBody
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:350)
	at org.kframework.backend.java.kil.KItem.accept(KItem.java:556)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:337)
	at org.kframework.backend.java.kil.BuiltinMap.accept(BuiltinMap.java:144)
	at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:402)
	at org.kframework.backend.java.kil.MapLookup.accept(MapLookup.java:122)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:307)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.accept(SymbolicConstraint.java:1506)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.translateConstraint(KILtoSMTLib.java:123)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.checkUnsat(SymbolicConstraint.java:837)
	at org.kframework.backend.java.kil.ConstrainedTerm.unifyImpl(ConstrainedTerm.java:263)
	at org.kframework.backend.java.kil.ConstrainedTerm.unify(ConstrainedTerm.java:213)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.getUnificationResults(SymbolicRewriter.java:384)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:243)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:293)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:666)
	at org.kframework.backend.java.symbolic.JavaSymbolicKRun.prove(JavaSymbolicKRun.java:209)
	at org.kframework.krun.KRunFrontEnd.normalExecution(KRunFrontEnd.java:132)
	at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:491)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:40)
	at org.kframework.main.Main.main(Main.java:86)
Exception in thread "main" java.lang.ClassCastException: org.kframework.backend.java.kil.ListLookup cannot be cast to org.kframework.backend.java.kil.SMTLibTerm
	at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:307)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.accept(SymbolicConstraint.java:1506)
	at org.kframework.backend.java.symbolic.KILtoSMTLib.translateConstraint(KILtoSMTLib.java:123)
	at org.kframework.backend.java.symbolic.SymbolicConstraint.checkUnsat(SymbolicConstraint.java:837)
	at org.kframework.backend.java.kil.ConstrainedTerm.unifyImpl(ConstrainedTerm.java:263)
	at org.kframework.backend.java.kil.ConstrainedTerm.unify(ConstrainedTerm.java:213)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.getUnificationResults(SymbolicRewriter.java:384)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:243)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:293)
	at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:666)
	at org.kframework.backend.java.symbolic.JavaSymbolicKRun.prove(JavaSymbolicKRun.java:209)
	at org.kframework.krun.KRunFrontEnd.normalExecution(KRunFrontEnd.java:132)
	at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:491)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:40)
	at org.kframework.main.Main.main(Main.java:86)
```
If you trace this through the code you find this is because implies fails on the final terms and continues to execute because of the following line of code on line 161 of ConstrainedTerm.java:matchImplies:

```
final Set<Variable> variables = unificationConstraint.variableSet();
        variables.removeAll(variableSet());
        unificationConstraint.orientSubstitution(variables);
        if (unificationConstraint.isFalse()
                || !unificationConstraint.substitution().keySet().containsAll(variables)) {
            return null;
        }
```

OrientSubstitution is not including one of the variables in the substitution, so the second clause of the boolean expression fails, and null is returned.

If this is a bug, I can create an issue for it and assign it to you.