fact: Definition bar (b : bool) : code fset0 [interface] nat_choiceType := {code if b then ret 0 else ret 1}.
imports: Coq(Utf8) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) extructures(ord fset fmap) Crypt(RulesStateProb Package Prelude) Equations(Equations)