add lookup_take_Some

Merged Ralf Jung requested to merge ralf/lookup_take_Some into master

another bit from Simuliris, original proof by @msammler

Edited by Ralf Jung

Merge request reports