<div dir="ltr"><div><div>Hi Joe,<br><br></div>I have not had time to investigate this 
thoroughly yet, but I have a suspicion that the redundant import check 
might not check for constants that don't appear in any theorems. 
Therefore, removing a "redundant" import might result in two different 
constants with the same name. Do you think this is possible?<br><br></div><div>Cheers,<br></div>Ramana</div>