proposition: Lemma get_raw_package_op_ext {L1 L2} {I E} {o : opsig} (hin : o \in E) (arg : src o) (p : raw_package) (hp1 : ValidPackage L1 I E p) (hp2 : ValidPackage L2 I E p) : (get_raw_package_op p hp1 o hin arg).(prog) = (get_raw_package_op p hp2 o hin arg).(prog).
proof: Proof. destruct (lookup_op p o) as [f|] eqn:e. 2:{ eapply from_valid_package in hp1 as H. specialize (H o hin). destruct o as [id [S T]]. destruct H as [f [H1 H2]]. unfold lookup_op in e. rewrite H1 in e. destruct choice_type_eqP. 2:{ noconf ef. congruence. } destruct choice_type_eqP. 2:{ noconf ef. congruence. } discriminate. } rewrite (get_raw_package_op_lookup p _ o hin arg f e). rewrite (get_raw_package_op_lookup p _ o hin arg f 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)