proposition: Lemma inversion_valid_opr : ∀ {A o x k}, @valid_code A (opr o x k) → (o \in import) * (∀ v, valid_code (k v)).
proof: Proof. intros A o x k h. dependent destruction h. intuition 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)