proposition: Lemma arbitrary1 (N : altMonad) (T : UU0) (def : T) h : arbitrary def [:: h] = Ret h :> N T.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)