proposition: Lemma domm_trim : ∀ E p, fsubset (domm (trim E p)) (idents E).
proof: Proof. intros E p. unfold trim. unfold idents. apply fsubset_ext. cbn. intros x h. rewrite mem_domm in h. rewrite filtermE in h. destruct (p x) as [[S' [T' f]]|] eqn:e. 2:{ rewrite e in h. cbn in h. discriminate. } rewrite e in h. cbn in h. destruct ((x, (S', T')) \in E) eqn:e1. 2:{ rewrite e1 in h. discriminate. } eapply mem_imfset in e1. exact e1. 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)