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