proposition: Lemma link_trim_right : ∀ L I E p1 p2, ValidPackage L I E p1 → link (trim E p1) (trim I p2) = link (trim E p1) p2.
proof: Proof. intros L I E p1 p2 h. apply eq_fmap. intro n. unfold link. rewrite !mapmE. destruct (trim E p1 n) as [[S1 [T1 f1]]|] eqn:e. 2:{ rewrite e. reflexivity. } rewrite e. cbn. f_equal. f_equal. f_equal. extensionality x. apply trim_get_inv in e as [e he]. eapply from_valid_package in h. specialize (h _ he). cbn in h. destruct h as [f [ef h]]. rewrite ef in e. noconf e. eapply code_link_trim_right. apply h. 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)