fact: Record osym_module : Type := OSymModule { carrier :> eqType; spec : osym_module_mixin carrier }.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)