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

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