Refine_Imperative_HOL.Structured_Apply