proposition: Lemma bindE (A B : Type) m (f : A -> [the monad of acto] B) : m >>= f = fun s => \bigcup_(i <- (fun x : [choiceType of choice_of_Type A * choice_of_Type S] => f x.1 x.2) @` (m s)) i.
proof: Proof. apply boolp.funext => s. rewrite bindE /= /join_of_bind /= /bind /=. set lhs := [fset _ _ | _ in _]. set rhs := [fset _ _ | _ in _]. rewrite (_ : lhs = rhs) //; apply/fsetP => x; rewrite {}/lhs {}/rhs. apply/idP/imfsetP => /=. - case/imfsetP => -[a1 a2] /=. rewrite /actm /= /map /=. case/bigfcupP' => /= b. case/imfsetP => -[b1 b2] /= Hb ->{b} /fset1P[-> -> ->{x a1 a2}]. by exists (b1, b2). - case=> -[a1 s1] Ha /= ->{x}. apply/imfsetP => /=. rewrite /actm /= /map /=. eexists. + apply/bigfcupP' => /=. eexists. apply/imfsetP => /=. by exists (a1, s1). by apply/fset1P; reflexivity. + by []. Qed.
imports: JMeq mathcomp(all_ssreflect) mathcomp(finmap) mathcomp(classical_sets) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer