fact: Fixpoint chElement_ordType (U : choice_type) : ordType := match U with | chUnit => unit_ordType | chNat => nat_ordType | chBool => bool_ordType | chProd U1 U2 => prod_ordType (chElement_ordType U1) (chElement_ordType U2) | chMap U1 U2 => fmap_ordType (chElement_ordType U1) (chElement_ordType U2) | chOption U => option_ordType (chElement_ordType U) | chFin n => [ordType of ordinal n.(pos) ] end.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)