proposition: Lemma opaque_me : ∀ {B L I E} (p : raw_package) (hp : valid_package L I E p) (o : opsig) (ho : o \in E) (arg : src o) (e : lookup_op p o = None), B.
proof: Proof. intros B L I E p hp o ho arg e. exfalso. destruct o as [n [S T]]. cbn - [lookup_op] in e. eapply from_valid_package in hp. specialize (hp _ ho). cbn in hp. destruct hp as [f [ef hf]]. cbn in e. destruct (p n) as [[St [Tt g]]|] eqn:e2. 2: discriminate. destruct choice_type_eqP. 2:{ noconf ef. congruence. } destruct choice_type_eqP. 2:{ noconf ef. congruence. } discriminate. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)