Various improvements to `Permutation` lemmas and instances

Various changes to Permutation lemmas:

• Rename Permutation_nil → Permutation_nil_r and and Permutation_singleton → Permutation_singleton_r.
• Add lemmas Permutation_nil_l and Permutation_singleton_l.
• Add new instance cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k)..
• Add lemma Permutation_cross_split.
• Make lemma elem_of_Permutation a biimplication

Also, I made the following changes that should not affect users:

• Name Proper and Inj instances for Permutation as operation_Permutation_{Proper,inj,inj_l,inj_r}
• Remove Proper instances for :: and ++ that are already supplied by the std lib.