proposition: Lemma arbitrary_inde (T : UU0) a (s : seq T) {U} (m : M U) : 0 < size s -> arbitrary a s >> m = m.
proof: Proof. elim: s a m => // h [_ a m _|h' t ih a m _]. by rewrite arbitrary1 bindretf. by rewrite arbitrary_cons // alt_bindDl ih // bindretf altmm. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)