algebra/ofe.v · ecd304f24f42f7a6d22bc279318e76c484e93409 · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago
ecd304f2
Internal definition of contractive and use it to prove internal_eq_rewrite. · ecd304f2
Robbert Krebbers authored 8 years ago
```
This removes Ralf's hack of using later_car, which is not function in the logic.

Thanks to Aleš for suggesting this.
```
ecd304f2

History
Internal definition of contractive and use it to prove internal_eq_rewrite.
Robbert Krebbers authored 8 years ago
```
This removes Ralf's hack of using later_car, which is not function in the logic.

Thanks to Aleš for suggesting this.
```