Skip to content
Snippets Groups Projects
Commit fead4470 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/eq_lemmas' into 'ci/refactor_staging' 

Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.

See merge request !526
parents 32edabf7 0a52e84c
No related branches found
No related tags found
2 merge requests!532Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming,!526Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.
Pipeline #91378 passed