fact: Definition stspPosetMixin := PosetMixin stsp_botP stsp_refl stsp_asym stsp_trans.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)