let decompose = EliminationTactics.decompose_tac
let demodulate = Saturation.demodulate_tac
let discriminate = DiscriminationTactics.discriminate_tac
let decompose = EliminationTactics.decompose_tac
let demodulate = Saturation.demodulate_tac
let discriminate = DiscriminationTactics.discriminate_tac