val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val assumption : ProofEngineTypes.tactic
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val assumption : ProofEngineTypes.tactic
val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic
val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
val compare : term:Cic.term -> ProofEngineTypes.tactic
val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic
val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
val compare : term:Cic.term -> ProofEngineTypes.tactic
val contradiction : ProofEngineTypes.tactic
val cut :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
val contradiction : ProofEngineTypes.tactic
val cut :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term -> ProofEngineTypes.tactic
val discriminate : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
Cic.term -> ProofEngineTypes.tactic
val discriminate : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic
val elim_type : term:Cic.term -> ProofEngineTypes.tactic
val exact : term:Cic.term -> ProofEngineTypes.tactic
val exists : ProofEngineTypes.tactic
val elim_type : term:Cic.term -> ProofEngineTypes.tactic
val exact : term:Cic.term -> ProofEngineTypes.tactic
val exists : ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term list -> ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term list -> ProofEngineTypes.tactic
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
unit -> ProofEngineTypes.tactic
val left : ProofEngineTypes.tactic
val letin :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
unit -> ProofEngineTypes.tactic
val left : ProofEngineTypes.tactic
val letin :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->