Factor antisymmetry proof for sublist

[andreasabel]

Commits:

• Simplify Sublist/Heterogeneous/antisym: collapse two cases:
  Removes an unnecessary case split.

• Simplify Sublist/Heterogeneous/antisym: factor out contradiction:
  Pulls the duplicated proof into a lemma.

These can be squashed, but I worked in two steps since I am unsure about the style policy.

[MatthewDaggitt]

Apart from that looks good to me!

[jamesmckinna]

Nitpicks (mostly cosmetic), but using implicits/variables makes proofs more robust (I think!?)

[jamesmckinna]

@andreasabel I would merge with my suggestions, unless you feel strongly that they make things worse?

Separately, you allude to (the possibility of) a default squash/merge policy for stdlib, and my git fu is weak in this regard: AFAIU, we squash commits while merging, but I'm conscious also that this is not the case for the main Agda codebase.

I'd be grateful for pointers to how to understand the trade offs between these approaches, and what conclusions, if any, we might draw for stdlib maintenance/development?

[andreasabel]

I committed your suggestions, thanks!

Merging by rebase would preserve the original commits. We do this in the Agda codebase if they are all meaningful and pass the build (and maybe the tests) individually. This can have the advantage of smaller commits too look at when bisecting which commit introduced a bug.
However, for the standard library there is probably no gain from small commits, so squashing is fine as default policy.