val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
unit -> ProofEngineTypes.tactic
val demodulate :
dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
unit -> ProofEngineTypes.tactic
val demodulate :
dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
val solve_rewrite :
universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val solve_rewrite :
universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic