fact: Example perm3 : qperm [:: 3; 2; 1] = Ret [:: 1; 2; 3] [~] Ret [:: 1; 3; 2] [~] Ret [:: 2; 1; 3] [~] Ret [:: 2; 3; 1] [~] Ret [:: 3; 1; 2] [~] Ret [:: 3; 2; 1] :> M (seq nat).
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)