Skip to content
  • Dmitry Khalanskiy's avatar
    Add a stronger version of `list_core_id`. · d6dbed9e
    Dmitry Khalanskiy authored
    A new lemma, `list_core_id'`, allows to infer that a list is
    `CoreId` by only checking that all its elements are `CoreId`, as
    opposed to the existing instance, `list_core_id`, that only works
    when the list contains elements of the type where every element is
    `CoreId`.
    d6dbed9e