proposition: Lemma iperm_rcons (A : eqType) t (x : A) : iperm (rcons t x) = iperm (x :: t) :> M _.
proof: Proof. by apply perm_eq_iperm; rewrite perm_rcons. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)