Skip to content

Added two proper instances with permutations

Michael Sammler requested to merge msammler/stdpp:feature/permutation_proper into master

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.

Merge request reports