This eases proofs, because lists computes. It also avoids issues with duplicates (so, no
more environment splitting judgment, just append).