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