Skip to content

Add local update lemmas for `discrete_fun` and `unit`.

Dan Frumin requested to merge dfrumin/iris-coq:local_updates into master

Some lemmas for the local update that we wrote with @amintimany

Merge request reports