proposition: Lemma domm_ID : ∀ I, domm (ID I) = fset (unzip1 I).
proof: Proof. intros I. apply eq_fset. intro x. rewrite in_fset. rewrite mem_domm. unfold ID. rewrite mkfmapE. rewrite getm_def_map_dep. rewrite -mkfmapE. rewrite -domm_mkfmap. rewrite mem_domm. destruct (mkfmap I x) eqn:e. - rewrite e. simpl. 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)