Refine_Imperative_HOL.Concl_Pres_Clarification