Definition foo : Set.
  Fail refine ($(abstract admit)$).