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