(* ring tactics *)
val ring_tac: ProofEngineTypes.tactic

  (* auxiliary tactics *)
val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val id_tac : ProofEngineTypes.tactic