let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)