proposition: Lemma valid_cmd_bind : ∀ {A B} (c : command A) (k : A → raw_code B), ValidCommand c → (∀ x, ValidCode (k x)) → ValidCode (cmd_bind c k).
proof: Proof. intros A B c k hc hk. unfold ValidCode in *. induction hc. - cbn. constructor. all: auto. - cbn. constructor. all: auto. - cbn. constructor. all: auto. - cbn. constructor. auto. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type) Equations.Prop.DepElim Equations(Equations)