let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
let contradiction () = apply_tactic NegationTactics.contradiction_tac
-let decompose ~clist = apply_tactic (EliminationTactics.decompose_tac ~clist)
+let decompose term = apply_tactic (EliminationTactics.decompose_tac ~term)
(*
let decide_equality () = apply_tactic VariousTactics.decide_equality_tac