* http://cs.unibo.it/helm/.
*)
+val isSetType: Cic.term -> bool
+exception EqualityNotDefinedYet (* raised by private_inversion_tac only *)
+val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic