val apply_tac:
  term: Cic.term -> ProofEngineTypes.tactic
val exact_tac:
  term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
  name: string -> ProofEngineTypes.tactic
val cut_tac:
  term: Cic.term -> ProofEngineTypes.tactic 
val letin_tac:
  term: Cic.term -> ProofEngineTypes.tactic 

val elim_intros_simpl_tac:
  term: Cic.term -> ProofEngineTypes.tactic