*)
val isSetType: Cic.term -> bool
-val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
+exception EqualityNotDefinedYet (* raised by private_inversion_tac only *)
+val private_inversion_tac: term: Cic.term -> bool list -> ProofEngineTypes.tactic
val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic