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