proposition: Lemma inversion_valid_cmd_bind : ∀ {A B} (c : command A) (k : A → raw_code B), ValidCode (cmd_bind c k) → ValidCommand c ∧ (∀ x, ValidCode (k x)).
proof: Proof. intros A B c k h. destruct c. - cbn. apply inversion_valid_opr in h. intuition auto. constructor. auto. - cbn. apply inversion_valid_getr in h. intuition auto. constructor. auto. - cbn. apply inversion_valid_putr in h. split. + constructor. intuition auto. + intros []. intuition auto. - cbn. split. + constructor. + intro. eapply inversion_valid_sampler in h. eauto. 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)