proposition: Lemma gettselectC A (s : seq A) B (f : _ -> _ -> M B) : (do ini <- get; do rs <- tselect s; f rs ini = do rs <- tselect s; do ini <- get; f rs ini)%Do.
proof: Proof. elim: s f => [|h t IH] f. by rewrite tselect_nil bindfailf; under eq_bind do rewrite bindfailf; rewrite bindmfail. case: t IH f => [|h' t] IH f. by rewrite tselect1 bindretf; under eq_bind do rewrite bindretf. rewrite tselect_cons // => H. rewrite [tselect _]lock. under eq_bind do rewrite alt_bindDl. rewrite [in RHS]alt_bindDl alt_bindDr. congr (_ [~] _). by rewrite bindretf; bind_ext => ?; rewrite bindretf. rewrite -lock. transitivity (do x0 <- tselect (h' :: t); do x <- get; f (x0.1, Tuple (fail_lib.tselect_cons_statement_obligation_2 h H x0)) x)%Do. rewrite -IH; bind_ext => x. by rewrite bindA; under eq_bind do rewrite bindretf. by rewrite bindA; bind_ext => y; rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib