proposition: Lemma map_loop_valid {T} {U A: choice_type} {L I} (s: seq T) (a: A) (c: T -> A -> raw_code (U × A)): (forall t a', ValidCode L I (c t a')) -> ValidCode L I (map_loop s a c).
proof: Proof. move=> H. elim: s => [|t s IHs] /= in a*. - by apply: valid_ret. - apply: valid_bind => ua1 /=. apply: valid_bind => ua2. by apply: valid_ret. 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)