[cinnamonheart]

Idris:

  data EndsWith : Type where
    EndsWithPeriod : (s: String) -> { auto prf : ("." `Strings.isSuffixOf` s = True) } -> EndsWith

  s : EndsWith
  s = EndsWithPeriod "."

  -- Value of type False = True cannot be found
  -- s2 : EndsWith
  -- s2 = EndsWithPeriod ""

The noun one might be possible -- I'm honestly less familiar with what a proper noun is offhand. (E: prefix=>suffix)