proposition: Lemma arbitrary_naturality (T U : UU0) (a : T) (b : U) (f : T -> U) : forall x, 0 < size x -> (M # f \o arbitrary a) x = (arbitrary b \o map f) x.
proof: Proof. elim=> // x [_ _ | x' xs /(_ isT)]. by rewrite [in LHS]compE fmapE bindretf. rewrite [in X in X -> _]/= fmapE => ih _. rewrite [in RHS]compE [in RHS]/= [in RHS](arbitrary_cons b) // [in LHS]compE. by rewrite [in LHS]arbitrary_cons // fmapE /= alt_bindDl bindretf /= ih. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)