1 val assume : string -> Cic.term -> ProofEngineTypes.tactic
2 val suppose : Cic.term -> string -> ProofEngineTypes.tactic
3 val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
4 val bydone : Cic.term -> ProofEngineTypes.tactic
5 val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic