Bring sequence axiomatization more in line with carbon to fix #629

[pieter-bos]

• Weakened triggers for singleton
• Placed append empty left/right in one quantifier
• Split index_over_append into left/right version, and used separate arithmetic functions
• Phrase disequality with skolem function for differing index

[mschwerhoff]

@marcoeilers Didn't you also recently port Carbon's axioms to Silicon?

[marcoeilers]

Yes, here: https://github.com/viperproject/silicon/tree/meilers_seq_set_axioms
That branch uses exactly Carbon's sequence, seq, and multiset axioms, in the same way. It's on the to-discuss-list for the next Viper meeting whether that's what we want.

[pieter-bos]

I'll close this under the assumption that it's still the plan to work on #642 at some point (though I understand it's difficult and/or not the highest priority). For what it's worth we still run into triggering problems with the default data structures occasionally, though not very often.