open Term
val disc_subset : types -> (types * types) option

module Coercion : Coercion.S