Commit 2024-09-18 01:17 d7e322a1

View on Github →

feat(List/Enum): add lemmas about ∀ x ∈ l.enum, p x etc (#16789)

Estimated changes

added theorem List.exists_mem_enum
added theorem List.forall_mem_enum