proposition: Lemma lookup_op_valid : ∀ L I E p o, ValidPackage L I E p → o \in E → ∃ f, lookup_op p o = Some f ∧ ∀ x, ValidCode L I (f x).
proof: Proof. intros L I E p o hp ho. eapply from_valid_package in hp. specialize (hp o ho). destruct o as [n [So To]]. destruct hp as [f [ef hf]]. exists f. intuition auto. cbn. destruct (p n) as [[St [Tt ft]]|] eqn:e. 2: discriminate. destruct choice_type_eqP. 2:{ inversion ef. congruence. } destruct choice_type_eqP. 2:{ inversion ef. congruence. } subst. cbn. noconf ef. reflexivity. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssreflect eqtype choice seq ssrfun ssrbool ssrnat) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb) Equations(Equations)