proposition: Lemma iperm_o_map (A B : UU0) (f : A -> B) : iperm \o map f = map f (o) iperm :> (_ -> M _).
proof: Proof. apply funext; elim => [/=|x xs IH]. by rewrite fcompE [iperm _]/= -[in RHS]compE (natural ret). by rewrite fcompE [in iperm _]/= fmap_bind -insert_map -bind_fmap -fcompE -IH. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)