proposition: Lemma perm_eq_arbitrary (A : eqType) def (a b : seq A) : perm_eq a b -> arbitrary def a = arbitrary def b :> M _.
proof: Proof. elim: a def b => [def b| h [|t1 t2] ih def b]. - by move/perm_size/esym/size0nil ->. - move: b => [/perm_size//|b1]; move => [|b2 b3 /perm_size//]. move/perm_consP => [i [s [ihb1s /perm_size/size0nil s0]]]. move: ihb1s; rewrite s0 /=. by move: i => [/=|i]; [rewrite rot0 => -[->]|rewrite /rot /= => -[->]]. - move=> htb. have [b1 [b2 bE]] : exists b1 b2, b = rcons b1 h ++ b2. suff : h \in b by exact: mem_rcons_cat. by move: htb => /perm_mem /(_ h); rewrite mem_head. rewrite bE arbitrary_cons // (ih _ (b1 ++ b2)); last first. move: htb; rewrite bE -cats1 -catA perm_sym (perm_catCA b1 [:: h] b2). by rewrite perm_cons perm_sym. move: b2 bE => [|b2 b3 bE]. rewrite !cats0. move: b1 => [bE|b1 b11]. by move: htb; rewrite bE => /perm_size. by rewrite -cats1 arbitrary_cat// arbitrary1 altC. rewrite [in RHS]arbitrary_cat ?size_rcons//. move: b1 => [//|b1 b11] in bE *. rewrite arbitrary_cat// altA; congr (_ [~] _). by rewrite -cats1 arbitrary_cat// arbitrary1 altC. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)