proposition: Lemma domm_ID_fset : ∀ I, domm (ID (fset I)) = fset (unzip1 I).
proof: Proof. intros I. rewrite domm_ID. apply eq_fset. intro x. rewrite !in_fset. unfold unzip1. apply/mapP. destruct (x \in [seq i.1 | i <- I]) eqn: e. - move: e => /mapP e. simpl in e. destruct e as [? h ?]. subst. simpl. eexists. 2: reflexivity. rewrite in_fset. auto. - move: e => /mapP e. simpl in e. intro h. apply e. destruct h as [? h ?]. rewrite in_fset in h. eexists. all: eauto. 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)