Skip to content
GitLab

relations lemmas

Merged Ralf Jung requested to merge ralf/relations into master

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

Edited by Ralf Jung