proposition: Lemma get_raw_package_op_lookup : ∀ {L} {I E : Interface} (p : raw_package) (hp : ValidPackage L I E p) (o : opsig) (ho : o \in E) (arg : src o) (f : src o -> raw_code (tgt o)) (H : lookup_op p o = Some f), (get_raw_package_op p hp o ho arg).(prog) = f arg.
proof: Proof. intros L I E p hp o ho arg f e. funelim (get_raw_package_op p hp o ho arg). 2:{ rewrite <- e1 in e. discriminate. } rewrite <- Heqcall. cbn. rewrite <- e1 in e. noconf e. reflexivity. 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)