Skip to content

relations lemmas

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

Merge request reports