Went through and revised the typing rules in thesis work. I think the proof of pattern spine injectivity is pretty solid now.