Tried formalizing this bit of math in twelf but hit a wall right at the end with a strengthening lemma that's too tedious for me to successfully prove.