Lookup total lemmas

This closes issue #50 (closed) and is a more complete alternative to !109 (closed).

This MR includes all lemmas that I think make sense. See also the discussion there.