Refine_Imperative_HOL.Sepref_Snip_Datatype