exception WrongUriToInductiveDefinition
exception ReferenceToDefinition
exception ReferenceToAxiom
exception ReferenceToVariable
exception ReferenceToCurrentProof
exception ReferenceToInductiveDefinition
val fdebug : int ref
val whd : Cic.term -> Cic.term
val are_convertible : Cic.term -> Cic.term -> bool