val assumption : unit -> unit
-val generalize : Cic.term -> unit
+val generalize :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ Cic.term list -> unit
val absurd : Cic.term -> unit
val contradiction : unit -> unit
(UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
Cic.term -> unit
-(*
+val injection : Cic.term -> unit
+val discriminate : Cic.term -> unit
val decide_equality : unit -> unit
-val compare : Cic.term -> Cic.term -> unit
-*)
+val compare : Cic.term -> unit
+
(*
val prova_tatticali : unit -> unit