proposition: Lemma tselect1 a : tselect [:: a] = Ret (a, [tuple]).
proof: Proof. rewrite /= bindfailf altmfail /tselect_obligation_1 /= tupleE /nil_tuple. by do 3 f_equal; apply eq_irrelevance. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)