proposition: Lemma get_raw_package_op_link {L} {I M E} {o : opsig} (hin : o \in E) (arg : src o) (p1 p2 : raw_package) (hp1 : ValidPackage L M E p1) (hpl : ValidPackage L I E (link p1 p2)) : (get_raw_package_op (link p1 p2) hpl o hin arg).(prog) = code_link ((get_raw_package_op p1 hp1 o hin arg).(prog)) p2.
proof: Proof. destruct (lookup_op (link p1 p2) o) as [f|] eqn:e. 2:{ eapply from_valid_package in hpl 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 (link p1 p2) _ o hin arg f e). destruct (lookup_op p1 o) as [fl|] eqn:el. 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 el. rewrite H1 in el. destruct choice_type_eqP. 2:{ noconf ef. congruence. } destruct choice_type_eqP. 2:{ noconf ef. congruence. } discriminate. } rewrite (get_raw_package_op_lookup p1 _ o hin arg fl el). apply (code_link_ext o hin arg p1 p2 fl el f e). 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)