proposition: Lemma id_link : ∀ L I E p, ValidPackage L I E p → trimmed E p → link (ID E) p = p.
proof: Proof. intros L I E p hp tp. apply eq_fmap. intro n. unfold link. rewrite mapmE. rewrite IDE. destruct getm_def as [[So To]|] eqn:e. - eapply getm_def_in in e as hi. eapply from_valid_package in hp. specialize (hp _ hi) as h'. cbn in h'. destruct h' as [f [ef hf]]. cbn. destruct (p n) as [[St [Tt g]]|] eqn:e1. 2: discriminate. destruct choice_type_eqP. 2:{ noconf ef. contradiction. } destruct choice_type_eqP. 2:{ noconf ef. contradiction. } subst. cbn. f_equal. f_equal. f_equal. extensionality x. apply bind_ret. - simpl. unfold trimmed in tp. destruct (p n) as [[St [Tt g]]|] eqn:e1. 1:{ eapply trimmed_valid_Some_in in e1 as hi. 2,3: eauto. exfalso. eapply in_getm_def_None. - exact hi. - cbn. auto. } 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)