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.