A formal framework for ASTRAL inter-level proof obbligations