Found the ex_loop
lemmas in Simuliris. Simuliris dos not actually need them any more, but they seem useful enough.
Proofs by @simonspies.
Found the ex_loop
lemmas in Simuliris. Simuliris dos not actually need them any more, but they seem useful enough.
Proofs by @simonspies.