Patch now that frame ∃ looks beneath definitions again

theories/concurrent_stacks/concurrent_stack3.v

theories/concurrent_stacks/concurrent_stack4.v

theories/lecture_notes/stack.v

theories/locks/freeable_lock/freeable_logatom_lock.v

theories/logatom/counter_with_backup/counter_proof.v

theories/logatom/flat_combiner/flat.v

theories/logatom/flat_combiner/peritem.v

theories/logatom/herlihy_wing_queue/hwq.v