proposition: Lemma fsval_eq : ∀ (A : ordType) (u v : {fset A}), FSet.fsval u = FSet.fsval v → u = v.
proof: Proof. intros A [u hu] [v hv] e. cbn in e. subst. f_equal. apply bool_irrelevance. 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)