theories/algebra/gmap.v · b4edc070b0645611980eb358d8dcab0bec713ab3 · Iris / Iris · GitLab

Find file Blame History Permalink

show that is f^2 is contractive, we can take the (unique) fixpoint of f · b4edc070
Ralf Jung authored Jan 25, 2017
```
Also add "Local" to some Default Proof Using to keep them more contained
```
b4edc070