theories/proofmode/reduction.v · 7ee248797524e139a116d699155f06cbc327f306 · Lennard Gäher / Iris · GitLab

Find file Blame History Permalink

make sbi_laterN compute and rely on that instead of MakeLaterN · 7ee24879
Ralf Jung authored Jul 04, 2018
```
With a pretty proof by Robbert
```
7ee24879