val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
val fourier_tac: ProofEngineTypes.tactic