A formal framework for ASTRAL intra-level proof obligations