Skip to content

add _wand lemmas for big-ops

Ralf Jung requested to merge ralf/big-wand into master

These seem so fundamental, so even though they are not hard to prove I was somewhat surprised that they do not already exist.

Merge request reports