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