This add a stage as a parameter to HbusFree.  This is to make it more
correct (this hypothesis is only true if we are in the Lsu), and forbid
from using it in theorems where it is not specialized.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>