Module Proofs.MX

module TO : sig ... end
module IsTO : sig ... end
module OrderTac : sig ... end