proposition: Lemma code_link_map_loop {T} {U A: choice_type} (s: seq T) (a: A) (c: T -> A -> raw_code (U × A)) p: code_link (map_loop s a c) p = map_loop s a (fun t a => code_link (c t a) p).
proof: Proof. elim: s => [// | t s IHs] /= in a*. rewrite code_link_bind. f_equal. apply: boolp.funext => ua1 /=. by rewrite code_link_bind IHs. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)