Time crunch, woo!
I think I have figured out the right generalization of the induction hypothesis for the injectivity proof. Tomorrow: massive writing effort.