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.
