proposition: Lemma trimmed_ID : ∀ I, trimmed I (ID I).
proof: Proof. intros I. unfold trimmed. apply eq_fmap. intro n. unfold trim. rewrite filtermE. destruct (ID I n) as [[S [T f]]|] eqn:e. - rewrite e. simpl. rewrite IDE in e. destruct (getm_def I n) as [[S' T']|] eqn:e'. 2: discriminate. cbn in e. noconf e. eapply getm_def_in in e'. rewrite e'. reflexivity. - rewrite e. 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)