proposition: Lemma notin_fset : ∀ (T : ordType) (s : seq T) (x : T), (x \notin fset s) = (x \notin s).
proof: Proof. intros T s x. unfold "\notin". rewrite in_fset. reflexivity. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq eqtype choice) extructures(ord fset fmap) Crypt(Prelude pkg_core_definition pkg_composition pkg_notation choice_type RulesStateProb) Coq(Utf8 FunctionalExtensionality Setoids.Setoid Classes.Morphisms) Equations(Equations)