proposition: Lemma link_trim_commut : ∀ E p1 p2, link (trim E p1) p2 = trim E (link p1 p2).
proof: Proof. intros E p1 p2. apply eq_fmap. intro n. unfold link. unfold trim. repeat rewrite ?filtermE ?mapmE. destruct (p1 n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity. cbn. destruct ((n, (S1, T1)) \in E) eqn:e1. 2:{ rewrite e1. cbn. reflexivity. } rewrite e1. cbn. 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)