Choice.Choicetype 't axioms_ = {choice_hasChoice_mixin : 't Coq_hasChoice.axioms_;eqtype_hasDecEq_mixin : 't Eqtype.Coq_hasDecEq.axioms_;}val choice_hasChoice_mixin : 'a1 axioms_ -> 'a1 Coq_hasChoice.axioms_type sort = __module Exports : sig ... end