You may have noticed that destruct (lookup x v) loses some information, resulting in unprovable statements if you're not careful. To keep the value of lookup x v as an extra hypothesis, use the destruct (lookup x v) eqn:H variant of destruct.

The proof is quite long, and your context may get messy very easily. Make sure to use the clear tactic to remove hypotheses that are not needed to have a better time navigating the proof. Renaming hypotheses also helps.

If c1 and c2 run to completion with recursion depth at most n and m, respectively, then c1; c2 only needs a recursion depth of S (max n m) to run to completion.