Key lemma for stack implementation