val assume : string -> NTacStatus.tactic_term -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
val suppose : NTacStatus.tactic_term -> string -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
val we_need_to_prove : NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term option -> 's NTacStatus.tactic
+val beta_rewriting_step : NTacStatus.tactic_term -> 's NTacStatus.tactic
val bydone : just -> 's NTacStatus.tactic
val by_just_we_proved : just -> NTacStatus.tactic_term -> string option -> NTacStatus.tactic_term
option -> 's NTacStatus.tactic