Added two proper instances with permutations

These are two Proper instances I found useful in my development. My original proofs use move => /Forall_cons[??] instead of inversion, but stdpp does not seem to use ssreflect and intros [??]%Forall_cons does not work for reasons I don't understand. So please let me know if you know how to do the prrof for Forall_proper_perm without inversion.

added 1 commit

• 8c1bbd99 - added two proper instance with permutations

Compare with previous version

resolved all discussions

added 1 commit

• 2c0bedd5 - added two proper instance with permutations

Compare with previous version

resolved all discussions

mentioned in commit 3c3ba0dd

merged

Merged, thanks.