Skip to content

Add a stronger version of `list_core_id`.

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.

Solves #258 (closed)

Edited by Dmitry Khalanskiy

Merge request reports