proposition: Lemma arbitrary2 (T : UU0) (def : T) h t : arbitrary def [:: h; t] = Ret h [~] Ret t :> M _.
proof: Proof. by rewrite /arbitrary /= altC. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)