(* 
val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
*)
val fourier_tac: ProofEngineTypes.tactic