proposition: Lemma link_id : ∀ L I E p, ValidPackage L I E p → flat I → trimmed E p → link p (ID I) = p.
proof: Proof. intros L I E p hp hI tp. apply eq_fmap. intro n. unfold link. rewrite mapmE. destruct (p n) as [[S [T f]]|] eqn:e. - cbn. f_equal. f_equal. f_equal. extensionality x. eapply trimmed_valid_Some_in in e as hi. 2,3: eauto. eapply from_valid_package in hp. specialize (hp _ hi) as h'. cbn in h'. destruct h' as [g [eg hg]]. rewrite e in eg. noconf eg. cbn in hg. eapply code_link_id. all: eauto. - reflexivity. 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)